Logiki nieklasyczne i ich zastosowania - zajęcia specjalnościowe WM-I-S1-E6-LIZ
Laboratorium (LAB) 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

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.