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

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.