Metody formalne w informatyce - zajecia specjalnościowe WM-I-S1-E5-MFI
Laboratorium (LAB) Semestr zimowy 2021/22

Ben-Ari, Logika dla Informatyków, WNT

Kolokwium oraz dwa projekty informatyczne.

1. Klasyczny rachunek zdań - wprowadzenie.

2. Postacie normalne formuł KRZ.

3. Rezolucja dla KRZ.

4. SAT solwery, zasada działania.

5. SAT solwery, wyrażanie własności.

6. Naturalna dedukcja dla KRZ.

7. Wprowadzenie do KRP - składnia i semantyka.

8. Wyrażanie własności w logice pierwszego rzędu.

9. Dowodzenie w teoriach pierwszego rzędu.

10. Automatyczne dowodzenie twierdzeń.

11. Automatyczne dowodzenie twierdzeń, cd.

12. Wyrażanie własnośći programów w logice Hoare'a.

13. Dowodzenie własności programów.

14. Automatyczne dowodzenie własności programów.

15. Automatyczne dowodzenie własności programów, cd.

Zajęcia łączą formułę ćwiczeń tablicowych oraz realizacji projektów informatycznych polegających na weryfikacji (dowodzeniu) wybranych własności programów przy pomocy narzędzi automatycznego dowodzenia.