Logika dla informatyków

Forma zajęć

Wykład (30 godzin) + laboratorium (30 godzin)

Autorzy

• Jerzy Tiuryn
• Jerzy Tyszkiewicz
• Paweł Urzyczyn

Wymagania wstępne

Konieczne

• Logika i teoria mnogości
• Automaty i obliczenia
• Matematyka dyskretna

Pożądane, ale niekonieczne

• 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