Logika dla informatyków

Forma zajęć

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

Sylabus

Autorzy

• Jerzy Tiuryn
• Jerzy Tyszkiewicz
• Paweł Urzyczyn

Wymagania wstępne

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

Zawartość

• Rachunek zdan.
  • Skladnia formul i semantyka zerojedynkowa.
  • Wzajemna wyrazalnosc spojnikow, funkcjonalna zupelnosc.
  • Postac normalna formuly tautologii.
  • Sila wyrazu logiki zdaniowej.
  • Informacja o SAT-solverach
• Logika pierwszego rzedu - cz.1: definicje
  • Formuly, zmienne wolne i zwiazane.
  • Spelnianie formul w strukturach relacyjnych, pojecie tautologii wynikania semantycznego.
  • Podstawienie i jego sens semantyczny.
• Logika pierwszego rzedu - cz. 2: sposob uzycia
  • Dyskusja waznych tautologii logiki pierwszego rzedu.
  • Preneksowa postac normalna i jej zastosowania
  • Logika formalna a zdania jezyka naturalnego.
• Logika pierwszego rzedu - cz. 3: ograniczenia
  • Nierozstrzygalnosc lgiki pierwszego rzedu.
  • Elementarna rownowaznosc struktur.
  • Gry Ehrenfeuchta-Fraissego.
• Paradygmaty dowodzenia:
  • styl Hilberta
  • naturalna dedukcja,
  • rachunek sekwentow.
  • Informacja o proverach
• Twierdzenie o Pelnosci dla rachunku zdan.
• Twierdzenie o Pelnosci dla rachunku predykatow.
• Teoria modeli
  • Twierdzenie o zwartosci i zastosowania
  • Twierdzenie Skolema-Lowenheima, niestandardowy model arytmetyki.
• Arytmetyka i tw. o niezpulenosci Goedla.
• Logiki programow
  • Składnia PDL
  • Twierdzenie o małym modelu dla PDL
  • Twierdzenie o pełności dla PDL
• Logika intuicjonistyczna
  • Konstruktywna interpretacja spojnikow
  • Semantyka w zbiorach otwartych (bez dowodu).
  • Formuly-typy, normalizacja dowodów jako proces obliczenia.
• Logika 2 rzedu
  • 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
  • Logiki wielowartościowe
  • Weryfikacja wspierana komputerowo