Logika, Wykład

Wykład 1 (5.X 2025)

Język rachunku zdań, naturalna dedukcja, drzewa dowodów w rachunku zdań, reguły dla spójników koniunkcji, implikacji, negacji, podwójnej negacji, dyzjunkcji, reguły pochodne, reguła dowodu niewprost, prawo wyłączonego środka.

Wykład 2 (19.X 2025)

Intuicjonizm a logika klasyczna.

Rachunek predykatów: język (funkcje, relacje, termy, formuły), zmienne związane i wolne, podstawienie.

Reguły naturalnej dedukcji dla równości i kwantyfikatorów.

Wykład 3 (26.X 2025)

Semantyka rachunku zdań logiki klasycznej i logiki intuicjonistycznej, struktury Kripkego, poprawność i pełność rachunku zdań.

Wykład 4 (16.XI 2025)

Semantyka rachunku predykatów (modele i środowiska), poprawność i pełność logiki predykatów.
Nierozstrzygalność, logika II rzędu, przykład z SQL.

Wykład 5 (23.XI 2025)

Weryfikacja modelowa, logika temporalna (czasu liniowego), systemy tranzycji.
LTL, przykłady.

Wykład 6 (7.XII 2025)

Logiki temporalne CTL i CTL*, zależności pomiędzy trzema logikami temporalnymi.

Wykład 7 (14.XII 2025)

Alloy -- system modelowania software'u.

Wykład 8 (11.I 2026)

Practical Alloy.

Wykład 9 (18.I 2026)

Algorytmy weryfikacji problemu SAT.
Algorytmy weryfikacji modelowej dla logik CTL oraz LTL.

Wykład 10 (1.II 2026)

Podsumowanie wykładów.

Egzamin termin zerowy.

Egzamin ustny: 14.II 2026, godz. 10:15, s. A218.
Szczegółowa lista na egzamin.