Metody formalne w informatyce - zajecia specjalnościowe WM-I-S1-E5-MFI
Wykład (WYK) Semestr zimowy 2022/23

Literatura podstawowa

1. Ben-Ari, Logika dla informatyków, WNT.

Literatura uzupełniająca

1. Yves Bertot, Coq in hurry, 2017, url: https://hal.inria.fr/inria-00001173/en/

2. Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program De-velopment, Coq'Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004. url: http://www.labri.fr/Perso/%7Ecasteran/CoqArt/index.html

3. Francois Bobot et al., The Why3 platform, 2022, url: https://why3.lri.fr/doc/

1. Klasyczny rachunek zdań (KRZ) - język i semantyka.

2. Postacie normalne formuł KRZ, rezolucja.

3. SAT solwery - wprowadzenie.

4. SAT solwery - modelowanie problemów.

5. System dowodzenia dla KRZ - naturalna dedukcja.

6. Logika pierwszego rzędu (klasyczny rachunek predykatów, KRP) - język.

7. Semantyka KRP.

8. System dowodzenia dla KRP - naturalna dedukcja.

9. System automatycznego dowodzenia twierdzeń, Coq.

10. System automatycznego dowodzenia twierdzeń - cd.

11. Semantyka programów.

12. Logika Hoare'a.

13. Dowodzenie własności programów, najsłabszy warunek początkowy, niezmienniki pętli.

14. System automatycznego dowodzenia własności programów, Why3.

15. System automatycznego dowodzenia własności programów - cd.