Logika dla informatyków
Informacje ogólne
Typ:obowiazkowyKierunek:Informatyka studia drugiego stopnia
Semestr:1
Wymiar zajęć:30 godzin wykładu, 30 godzin ćwiczeń
Punkty ECTS:8
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.
