Logiki nieklasyczne i ich zastosowania - zajęcia specjalnościowe WM-I-S1-E6-LIZ
Laboratorium (LAB) Semestr letni 2023/24

Literatura podstawowa

1. 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

2. 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

1. Michael Huth, Mark Ryan, Logic in Computer Science. Modelling and Reasoning about Systems. 2004

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

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

3. 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

4. Moshe Y. Vardi, From Philosophical to Industrial Logics,

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

5. Philip Wadler, Propositions as Types, 2015,

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

Zajęcia 1-3

Klasyczny rachunek zdań. Logiki wielowartościowe: logika Łukasiewicza, logiki Kleenego, trójwartościowa logika SQL.

Semantyka algebraiczna.

Zajęcia 4-6

Logiki modalne. Systemy logik modalnych.

Semantyka Krikpkego. Pełność.

Zajęcia 7-9

Logika LTL (Linear Time Logic).

Semantyka LTL. Wyrażanie własności w logice LTL.

Zajęcia 10-12

Sytem NuSMV, teorio-modelowa weryfikacja własności systemów informatycznych.

Zajęcia 13

Logika CTL (Computation Tree Logic).

Wyrażanie własnośći w logice CTL.

Weryfikacja własnośći systemów w logice CTL przy pomocy NuSMV.

Zajęcia 14

Intuicjonistyczny rachunek zdań. Semantyka.

Zajęcia 15

Logiki rozmyte.