Metody formalne w informatyce - zajecia specjalnościowe WM-I-S1-E5-MFI
Laboratorium (LAB) 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).

2. Postacie normalne CNF i DNF.

3. Rezolucja.

4. SAT solvery.

5. SAT solvery.

6. Naturalna dedukcja dla KRZ.

7. Podstawy Coq'a.

8. Podstawy Coq'a, ciąg dalszy.

9. Logika pierwszego rzędu.

10. Logika pierwszego rzędu, naturalna dedukcja i Coq.

11. Logika Hoare'a.

12. Logika Hoare'a, ciąg dalszy.

13. Podstawy systemu Why3.

14. Podstawy systemu Why3, weryfikacja programów.

15. Podstawy systemu Why3, weryfikacja programów.