Logika dla informatyków

Forma zajęć

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

Opis

Wykład logiki dla informatyków na poziomie magisterskim. Oprócz przedstawienia klasycznych pojęć i wyników logiki matematycznej i teorii modeli, zawiera wykłady poświęcone działom logiki silnie powiązanym z teoretyczną informatyką.

Sylabus

Autorzy

• Jerzy Tiuryn — Uniwersytet Warszawski
• Jerzy Tyszkiewicz — Uniwersytet Warszawski
• Paweł Urzyczyn — Uniwersytet Warszawski

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
  • tautologie rachunku zdań
  • postać normalna formuł
• 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-Fraïssé
• 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-Löwenheima, niestandardowy model arytmetyki
• Arytmetyka i twierdzenie o niezupełności Gödla
• 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
  • 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

Moduły

Wykład z logiki w formacie PDF

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