Logiki nieklasyczne i ich zastosowania - zajęcia specjalnościowe WM-I-S1-E6-LIZ
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.
Dyscyplina naukowa, do której odnoszą się efekty uczenia się
E-Learning
W cyklu 2021/22_L: E-Learning (pełny kurs) z podziałem na grupy | W cyklu 2022/23_L: E-Learning (pełny kurs) z podziałem na grupy | W cyklu 2024/25_L: E-Learning | W cyklu 2023/24_L: E-Learning |
Grupa przedmiotów ogólnouczenianych
Opis nakładu pracy studenta w ECTS
W cyklu 2022/23_L: Wykład:
uczestnictwo w zajęciach, 30h
praca własna, lektury, pogłębienie wiedzy, 40h
Razem: 70h, 3 ECTS.
Laboratorium
uczestnictwo w zajęciach, 30h
praca własna, nauka programów wykonujących model checking, tworzenie modeli w tych programach, 40h
Razem: 70h, 3 ECTS | W cyklu 2023/24_L: Wykład:
uczestnictwo w zajęciach, 30h
praca własna, lektury, pogłębienie wiedzy, 45h
Razem: 75h, 3 ECTS.
Laboratorium
uczestnictwo w zajęciach, 30h
praca własna, nauka programów wykonujących model checking, tworzenie modeli w tych programach, 45h
Razem: 75h, 3 ECTS |
Poziom przedmiotu
Symbol/Symbole kierunkowe efektów uczenia się
Typ przedmiotu
Wymagania wstępne
Koordynatorzy przedmiotu
W cyklu 2021/22_L: | W cyklu 2023/24_L: | W cyklu 2024/25_L: | W cyklu 2022/23_L: |
Efekty kształcenia
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).
Kryteria oceniania
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ą.
Więcej informacji
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: