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

założenia

1. Rachunek zdań (Ćwiczenia)
2. Język logiki pierwszego rzędu (Ćwiczenia) TR
3. Logika pierwszego rzędu. Sposób użycia (Ćwiczenia) TR
4. Ograniczenia logiki pierwszego rzędu (Ćwiczenia)AS
5. Paradygmaty dowodzenia (Ćwiczenia)
6. Pełność rachunku zdań (Ćwiczenia)AS
7. Pełność rachunku predykatów (Ćwiczenia)AS
8. Teoria modeli (Ćwiczenia) TR
9. Arytmetyka pierwszego rzędu (Ćwiczenia) TR
10. Zdaniowa logika dynamiczna (Ćwiczenia)
11. Logika intuicjonistyczna (Ćwiczenia)
12. Logika drugiego rzędu (Ćwiczenia)
13. Logika w informatyce (Ćwiczenia)AS