Logika dla informatyków

Forma zajęć

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

Opis

Zastosowanie metod i narzędzi logiki matematycznej w informatyce.

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 zdań.
  • Składnia formuł i semantyka zerojedynkowa.
  • Wzajemna wyrażalność spójników, funkcjonalna zupełność.
  • Postać normalna formuły tautologii.
  • Siła wyrazu logiki zdaniowej.
• 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-Fraissego.
• 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-Lowenheima, niestandardowy model arytmetyki.
• Arytmetyka i tw. o niezupełności Goedla.
• 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 (bez dowodu).
  • 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 tw. Fagina i Stockmeyera
  • Informacja o tw. Rabina
• Logika w informatyce
  • Logiki wielowartościowe
  • Tw. Codda
  • Rozstrzygalnośc teorii logicznych

Moduły

Wykład z logiki w formacie PDF