108 systemów wspomagania specyfikacji i weryfikacji oprogramowania i hardware'u.

Wykład 1 (14.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 (21.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 (28.X 2025)

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

Wykład 4 (4.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 (18.XI 2025)

Weryfikacja modelowa, logika temporalna (czasu liniowego), systemy tranzycji.

Wykład 6 (25.XI 2025)

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

Wykład 7 (2.XII 2025)

Algorytmy weryfikacji modelowej dla logik CTL oraz LTL.

Wykład 8 (9.XII 2025)

System SPIN.
Przykładowe programy.

Wykład 9 (16.XII 2025)

Alloy -- system modelowania software'u.

Wykład 10 (23.XII 2025)

Alloy -- system modelowania software'u.

Wykład 11 (13.I 2026)

Practical Alloy.

Wykład 12 (20.I 2026)

Logika Hoare'a.

Algorytmy weryfikacji problemu SAT.

Wykład 13 (27.I 2026)

Podsumowanie wykładów.

Egzamin ustny: 10-11.II 2026, g. 11:00, s. A218.
Lista szczegółowa.