Logika dla informatyków


Informacje ogólne

Typ:obowiazkowy
Kierunek: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.