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

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. Semantyka programów.

11. Logika Hoare'a.

12. Logika Hoare'a, c.d.

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.