Non-classical logics and applications

Wykład będzie przeglądem logik nieklasycznych, w szczególności tych wykorzystywanych w informatyce.

Celem kursu jest zapoznanie studenta z wielością logik nieklasycznych oraz sposobów ich wykorzystania. Po jego ukończeniu student powinien być w stanie zamodelować system, np. skończenie stanowy, przy pomocy technik opartych o logiki nieklasyczne.

Studenci poznają logiki wielowartościowe i ich zastosowania, takie jak logika Kleene'go i trójwartościowa logika SQL. Następnie przedstawione zostaną logiki modalne wraz z semantyką Kripke'go oraz algebraiczną oraz ich zastosowania w sprawdzaniu poprawności programów (model checking). Omówiona też zostanie logika intuicjonistyczna (konstruktywna) oraz jej związki z rachunkiem lambda oraz izomorfizmem Curry'ego-Howard'a czyli odpowiedniością pomiędzy dowodami i programami.

Wykład:

MA1_W01 - rozumie rolę logik nieklasycznych w tworzeniu formalizacji i modelowania systemów,

MA1_W04 - zna podstawowe logiki nieklasyczne i ich własności formalne.

Laboratorium:

MA1_K01 - jest gotów do określania potrzeb w rozwoju swojej wiedzy,

MA1_K02 - potrafi świadomie określić brakujące elementy swojej wiedzy i zna sposoby jej rozwoju,

MA1_K07 - jest gotowy do oceny różnych sposobów wykorzystania logik nieklasycznych w modelowaniu systemów.

Dla wszystkich efektów przyjmuje się następujące kryteria oceny we wszystkich formach weryfikacji:

ocena 5: osiągnięty w pełni (bez uchwytnych niedociągnięć)

ocena 4,5: osiągnięty niemal w pełni i nie są spełnione kryteria przyznania wyższej oceny

ocena 4: osiągnięty w znacznym stopniu i nie są spełnione kryteria przyznania wyższej oceny

ocena 3,5: osiągnięty w znacznym stopniu

z wyraźną przewagą pozytywów i nie są spełnione kryteria

przyznania wyższej oceny

ocena 3: osiągnięty dla większości przypadków objętych weryfikacją i nie są spełnione kryteria przyznania

wyższej oceny

ocena 2: nie został osiągnięty dla większości przypadków objętych weryfikacją