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.

Uwaga: wykład w dniu 23.XII zdalny w technologii Teams
link do spotkania
identyfikator spotkania: 361 139 770 552 29
kod dostępu: ty2jV7BV