Logiki nieklasyczne i ich zastosowania - zajęcia specjalnościowe WM-I-S1-E6-LIZ
Wykład (WYK) Semestr letni 2022/23

Literatura podstawowa

Ze Hou, Fundamentals of Logic and Computation

With Practical Automated Reasoning and Verification, Srpinger, 2021

url: https://link.springer.com/book/10.1007/978-3-030-87882-5

Anita Wasilewska, Logics for Computer Science, Springer, 2018.

url: https://link.springer.com/book/10.1007/978-3-319-92591-2

Literatura uzupełniająca

Michael Huth, Mark Ryan, Logic in Computer Science. Modelling

and Reasoning about Systems. 2004

Mordechai Ben-Ari, Principles of the SPIN Model Checker, 2008

url: https://link.springer.com/book/10.1007/978-1-84628-770-1

Seiki AkamaTetsuya MuraiYasuo Kudo,

Reasoning with Rough Sets

Logical Approaches to Granularity-Based Framework

(w szczególności rozdział Non-classical Logics),

2018.

url: https://link.springer.com/book/10.1007/978-3-319-72691-5

Moshe Y. Vardi, From Philosophical to Industrial Logics,

url: https://www.cs.rice.edu/~vardi/papers/icla09.pdf

Philip Wadler, Propositions as Types, 2015,

url: https://dl.acm.org/action/downloadSupplement?doi=10.1145%2F2699407&file=p75-wadler-supp.pdf

1. Wprowadzenie i motywacje.

Dlaczego logika klasyczna nam nie wystarcza?

Historia logik nieklasycznych, wykorzystanie logik nieklasycznych w informatyce.

2. Logiki wielowartościowe.

Historia i motywacje (Arystoteles i Łukasiewicz).

Algebra wartości logicznych. ]

Podstawowe systemy logik wielowartościowych.

Logika Kleene'go, logika SQL.

3. Logiki modalne

Motywacje: epistemiczna, konieczność, dowodliwość.

Składnia zdaniowej logiki modalnej.

Podstawowe systemy logik modalnych.

Semantyka Kripke'go.

4. Semantyka Kripke'go c.d.

Twierdzenia o pełności.

Algebraiczna semantyka logik modalnych.

Interpretacja konieczności jako dowodliwości.

Twierdzenia Godl'a o niezupełności.

5. Logiki modalne czasu liniowego: CTL, LTL.

Złożoność logik modalnych.

6. Automaty skończone, omega-automaty.

Złożoność problemów automatowych.

7. Wprowadzenie do model checking.

Modelowanie systemów informatycznych za pomocą struktur Kripke'owskich.

8. Wyrażanie własności systemów informatycznych za pomocą CTL, LTL.

Safety, liveness.

9. Narzędzia informatyczne do weryfikacji modelowej. SPIN.

10. Narzędzia informatyczne do weryfikacji modelowej, SPIN, c.d.

11. Logika intuicjonistyczna.

Motywacje. Intuicjonistyczny rachunek zdań IPC.

Semantyka Kripkego dla IPC.

12. System dowodzenia dla IPC.

Twierdzenie o pełności.

Semantyka algebraiczna i twierdzenie o pełności.

13. Rachunek lambda. Isomorfizm Currego-Howarda.

14. Isomorfizm Currego-Howarda, generowanie programów, programowanie funkcyjne.

15. Logika liniowa, logika rozmyta, zbiory rozmyte.