MIMINF: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 — Uniwersytet Warszawski
• Jerzy Tyszkiewicz — Uniwersytet Warszawski
• Paweł Urzyczyn — Uniwersytet Warszawski

Wymagania wstępne

• Logika i teoria mnogości
• Języki, 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 twierdzenie 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 twierdzeniu Fagina i Stockmeyera
  • informacja o twierdzeniu Rabina
• Logika w informatyce:
  • logiki wielowartościowe
  • twierdzenie Codda
  • rozstrzygalność teorii logicznych