Logika dla informatyków: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
Diks (dyskusja | edycje)
538 edycji
 
(Nie pokazano 38 wersji utworzonych przez 7 użytkowników)
Linia 4: Linia 4:


=== Opis ===
=== Opis ===
Wykład logiki dla informatyków na poziomie magisterskim. Oprócz przedstawienia klasycznych pojęć i wyników logiki matematycznej i teorii modeli, zawiera wykłady poświęcone działom logiki silnie powiązanym z teoretyczną informatyką.


 
== Sylabus ==
=== Sylabus ===


=== Autorzy ===
=== Autorzy ===


* Jerzy Tiuryn
* Jerzy Tiuryn — Uniwersytet Warszawski
* Jerzy Tyszkiewicz  
* Jerzy Tyszkiewicz — Uniwersytet Warszawski
* Paweł Urzyczyn
* Paweł Urzyczyn — Uniwersytet Warszawski


=== Wymagania wstępne ===
=== Wymagania wstępne ===
===== Konieczne =====


* Logika i teoria mnogości
* Logika i teoria mnogości
* Automaty i obliczenia
* Automaty i obliczenia
* Matematyka dyskretna
* Matematyka dyskretna
===== Pożądane, ale niekonieczne =====
* Bazy danych
* Bazy danych
* Programowanie funkcyjne
* Programowanie funkcyjne
Linia 30: Linia 25:
=== Zawartość ===
=== Zawartość ===


* Rachunek zdan.
* Rachunek zdań:
** Skladnia formul i semantyka zerojedynkowa.
** składnia formuł i semantyka zerojedynkowa
** Wzajemna wyrazalnosc spojnikow, funkcjonalna zupelnosc.
** tautologie rachunku zdań
** Postac normalna formuly tautologii.
** postać normalna formuł
**  Sila wyrazu logiki zdaniowej.
* Logika pierwszego rzędu - cz.1: definicje:
** Informacja o SAT-solverach
** formuły, zmienne wolne i związane
 
** spełnianie formul w strukturach relacyjnych, pojecie tautologii, wynikania semantycznego
* Logika pierwszego rzedu - cz.1: definicje
** podstawienie i jego sens semantyczny
** Formuly, zmienne wolne i zwiazane.
* Logika pierwszego rzędu - cz. 2: sposób użycia:
** Spelnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.
** dyskusja ważnych tautologii logiki pierwszego rzędu
** Podstawienie i jego sens semantyczny.
** preneksowa postać normalna i jej zastosowania  
 
** logika formalna a zdania języka naturalnego
* Logika pierwszego rzedu - cz. 2: sposob uzycia
* Logika pierwszego rzędu - cz. 3: ograniczenia:
** Dyskusja waznych tautologii logiki pierwszego rzedu.
** nierozstrzygalność logiki pierwszego rzędu
** Preneksowa postac normalna i jej zastosowania  
** elementarna równoważność struktur
** Logika formalna a zdania jezyka naturalnego.
** gry Ehrenfeuchta-Fraïssé
 
* Logika pierwszego rzedu - cz. 3: ograniczenia
** Nierozstrzygalnosc lgiki pierwszego rzedu.
** Elementarna rownowaznosc struktur.
** Gry Ehrenfeuchta-Fraissego.
 
* Paradygmaty dowodzenia:  
* Paradygmaty dowodzenia:  
** styl Hilberta
** styl Hilberta
** naturalna dedukcja,
** naturalna dedukcja
** rachunek sekwentow.
** rachunek sekwentów
** Informacja o proverach
* Twierdzenie o pełności dla rachunku zdań
 
* Twierdzenie o pełności dla rachunku predykatów
* Twierdzenie o Pelnosci dla rachunku zdan.
* Teoria modeli:
 
** twierdzenie o zwartości i zastosowania
* Twierdzenie o Pelnosci dla rachunku predykatow.
** twierdzenie Skolema-Löwenheima, niestandardowy model arytmetyki
 
* Arytmetyka i twierdzenie o niezupełności Gödla
* Teoria modeli
* Logiki programów:
** Twierdzenie o zwartosci i zastosowania
** składnia PDL
** Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
** twierdzenie o małym modelu dla PDL
**
** twierdzenie o pełności dla PDL
 
* Logika intuicjonistyczna:
 
** konstruktywna interpretacja spójników
* Arytmetyka i tw. o niezpulenosci Goedla.
** semantyka w zbiorach otwartych
 
** formuły-typy, normalizacja dowodów jako proces obliczenia
* Logiki programow
* Logika 2 rzędu:
** Składnia PDL
** definicja, podstawowe własności.
** Twierdzenie o małym modelu dla PDL
** równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** Twierdzenie o pełności dla PDL
** informacja o twierdzeniu Fagina i Stockmeyera
** informacja o twierdzeniu Rabina
* Logika w informatyce:
** logiki wielowartościowe
** twierdzenie Codda
** rozstrzygalność teorii logicznych


== Moduły ==


* Logika intuicjonistyczna
** Konstruktywna interpretacja spojnikow
** Semantyka w zbiorach otwartych (bez dowodu).
** Formuly-typy, normalizacja dowodów jako proces obliczenia.


* Logika 2 rzedu
[http://www.mimuw.edu.pl/~urzy/calosc.pdf Wykład z logiki w formacie PDF]
** Definicja, podstawowe własności.
** Informacja o semantyce Henkina i relacji do polimorfizmu
** Równoważnośc monadycznej logiki drugiego rzędu i automatów skończonych na słowach
** Informacja o tw. Fagina


* Wybrane zastosowania logiki w informatyce
<!--
** Tw. Codda
# [[Logika dla informatyków/Rachunek zdań|Rachunek zdań]] ([[Logika dla informatyków/Ćwiczenia 1|Ćwiczenia]])
** Logiki wielowartościowe
# [[Logika dla informatyków/Język logiki pierwszego rzędu|Język logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 2|Ćwiczenia]])
** Weryfikacja wspierana komputerowo
# [[Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia|Logika pierwszego rzędu. Sposób użycia]] ([[Logika dla informatyków/Ćwiczenia 3|Ćwiczenia]])
# [[Logika dla informatyków/Ograniczenia logiki pierwszego rzędu|Ograniczenia logiki pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 4|Ćwiczenia]])
# [[Logika dla informatyków/Paradygmaty dowodzenia|Paradygmaty dowodzenia]] ([[Logika dla informatyków/Ćwiczenia 5|Ćwiczenia]])
# [[Logika dla informatyków/Pełność rachunku zdań|Pełność rachunku zdań]] ([[Logika dla informatyków/Ćwiczenia 6|Ćwiczenia]])
# [[Logika dla informatyków/Pełność rachunku predykatów|Pełność rachunku predykatów]] ([[Logika dla informatyków/Ćwiczenia 7|Ćwiczenia]])
# [[Logika dla informatyków/Teoria modeli|Teoria modeli]] ([[Logika dla informatyków/Ćwiczenia 8|Ćwiczenia]])
# [[Logika dla informatyków/Arytmetyka pierwszego rzędu|Arytmetyka pierwszego rzędu]] ([[Logika dla informatyków/Ćwiczenia 9|Ćwiczenia]])
# [[Logika dla informatyków/Zdaniowa logika dynamiczna|Zdaniowa logika dynamiczna]] ([[Logika dla informatyków/Ćwiczenia 10|Ćwiczenia]])
# [[Logika dla informatyków/Logika intuicjonistyczna|Logika intuicjonistyczna]] ([[Logika dla informatyków/Ćwiczenia 11|Ćwiczenia]])
# [[Logika dla informatyków/Logika drugiego rzędu|Logika drugiego rzędu]] ([[Logika dla informatyków/Ćwiczenia 12|Ćwiczenia]])
# [[Logika dla informatyków/Logika w informatyce|Logika w informatyce]] ([[Logika dla informatyków/Ćwiczenia 13|Ćwiczenia]])
-->

Aktualna wersja na dzień 21:49, 5 lut 2007

Forma zajęć

Wykład (30 godzin) + ćwiczenia (30 godzin)

Opis

Wykład logiki dla informatyków na poziomie magisterskim. Oprócz przedstawienia klasycznych pojęć i wyników logiki matematycznej i teorii modeli, zawiera wykłady poświęcone działom logiki silnie powiązanym z teoretyczną informatyką.

Sylabus

Autorzy

  • Jerzy Tiuryn — Uniwersytet Warszawski
  • Jerzy Tyszkiewicz — Uniwersytet Warszawski
  • Paweł Urzyczyn — Uniwersytet Warszawski

Wymagania wstępne

  • Logika i teoria mnogości
  • Automaty i obliczenia
  • Matematyka dyskretna
  • Bazy danych
  • Programowanie funkcyjne
  • Złożoność obliczeniowa

Zawartość

  • Rachunek zdań:
    • składnia formuł i semantyka zerojedynkowa
    • tautologie rachunku zdań
    • postać normalna formuł
  • Logika pierwszego rzędu - cz.1: definicje:
    • formuły, zmienne wolne i związane
    • spełnianie formul w strukturach relacyjnych, pojecie tautologii, wynikania semantycznego
    • podstawienie i jego sens semantyczny
  • Logika pierwszego rzędu - cz. 2: sposób użycia:
    • dyskusja ważnych tautologii logiki pierwszego rzędu
    • preneksowa postać normalna i jej zastosowania
    • logika formalna a zdania języka naturalnego
  • Logika pierwszego rzędu - cz. 3: ograniczenia:
    • nierozstrzygalność logiki pierwszego rzędu
    • elementarna równoważność struktur
    • gry Ehrenfeuchta-Fraïssé
  • Paradygmaty dowodzenia:
    • styl Hilberta
    • naturalna dedukcja
    • rachunek sekwentów
  • Twierdzenie o pełności dla rachunku zdań
  • Twierdzenie o pełności dla rachunku predykatów
  • Teoria modeli:
    • twierdzenie o zwartości i zastosowania
    • twierdzenie Skolema-Löwenheima, niestandardowy model arytmetyki
  • Arytmetyka i twierdzenie o niezupełności Gödla
  • Logiki programów:
    • składnia PDL
    • twierdzenie o małym modelu dla PDL
    • twierdzenie o pełności dla PDL
  • Logika intuicjonistyczna:
    • konstruktywna interpretacja spójników
    • semantyka w zbiorach otwartych
    • formuły-typy, normalizacja dowodów jako proces obliczenia
  • Logika 2 rzędu:
    • definicja, podstawowe własności.
    • równoważność monadycznej logiki drugiego rzędu i automatów skończonych na słowach
    • informacja o twierdzeniu Fagina i Stockmeyera
    • informacja o twierdzeniu Rabina
  • Logika w informatyce:
    • logiki wielowartościowe
    • twierdzenie Codda
    • rozstrzygalność teorii logicznych

Moduły

Wykład z logiki w formacie PDF


Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Logika_dla_informatyków&oldid=69291”