Informacje ogólne

Typ:obowiazkowy

Program

• Rachunek zdań: naturalna dedukcja, język sformalizowany, semantyka, niesprzeczność i zupełność, postacie normalne, SAT solvers.
• Rachunek predykatów: język formalny, naturalna dedukcja, semantyka, nierozstrzygalność, wersje logiki II rzędu.
• Weryfikacja poprzez sprawdzanie modelowe (model checking): logiki temporalne, liniowa, czasu rozgałęzionego, algorytmy sprawdzania modelowego.
• Weryfikacja programów: logika Hoare'a, pojęcia częścowej i całkowitej poprawności, rachunek dowodów częściowej i całkowitej poprawności.
  

Sposób zaliczenia

Zaliczenie ćwiczeń: sprawdzian (w laboratorium komputerowym)umiejętności posłużenia się komputerowo wspomaganymi systemamidowodzenia i specyfikacji.
Zaliczenie przedmiotu: sprawdzian z jednego z systemów wspomaganiadowodzenia plus egzamin ustny z treści wykładu.Warunkiem przystąpienia do egzaminu jest zaliczenie ćwiczeń.

Literatura

• M. Huth, M. Ryan, Logic in Computer Science, Cambridge, 2004.