Logiki nieklasyczne i ich zastosowania - zajęcia specjalnościowe

informatyka techniczna i telekomunikacja

średnio-zaawansowany

Wykład: I1_W14, I1_U18

Laboratorium: I1_W14, I1_U18

Podstawy logiki i teorii mnogości. Podstawy programowania.

Wykład będzie przeglądem logik nieklasycznych wykorzystywanych w informatyce. Studenci poznają logiki wielowartościowe takie, jak logika Kleene'go oraz ich zastosowania, np. w języku SQL. Następnie przedstawione zostaną logiki modalne wraz z semantyką Kripke'go oraz algebraiczną, ich rozszrzenia LTL, CTL 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 isomorfizmem Curry'ego-Howard'a czyli odpowiedniością pomiędzy dowodami i programami.

Wykład

Student:

W1 - zna teoretyczne podstawy logik nieklasycznych oraz sposoby ich wykorzystania w informatyce (I1_W14),

U1 - potrafi stosować logiki nieklasyczne do modelowania własności systemów informatycznych (I1_U18).

Laboratorium

Student:

W1 - zna sposoby konstruowania modeli matematycznych dla systemów informatycznych (I1_W14),

U1 - potrafi posługiwać się oprogramowaniem wykorzystującym logiki modalne LTL, CTL oraz model checking (I1_U18).

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