Złożoność określania własności logicznych stwierdzeń 1000-2M23ZWL
Przedstawiona zostanie znana wiedza dotycząca zależności złożoności i rozstrzygalności problemów spełnialności i dowodliwości dla fragmentów logiki klasycznej i intuicjonistycznej. Każdy wykład będzie zawierał pełny dowód dla przykładowego problemu z danej grupy wraz z dyskusją na temat tego, jak taki dowód zaadaptować do pozostałych przypadków. Celem wykładu jest bardziej pokazanie, jakie mechanizmy pojawiają się przy określaniu własności stwierdzeń, niż podanie stabelaryzowanej wiedzy łączącej klasy złożoności z fragmentami logiki.
1. Składnia systemów logicznych
2. Semantyka systemów logicznych
3. Problem układanki i jego warianty
4. Złożoność w klasycznej logice zdaniowej
5. Złożoność w intuicjonistycznej logice zdaniowej
6. Nierozstrzygalne klasy w logice klasycznej bez równości i symboli funkcyjnych
7. Rozstrzygalne klasy w logice klasycznej bez równości i symboli funkcyjnych
8. Nierozstrzygalne klasy w logice intuicjonistycznej bez równości i symboli funkcyjnych
9. Rozstrzygalne klasy w logice intuicjonistycznej bez równości i symboli funkcyjnych
10. Nierozstrzygalne klasy w logice klasycznej z równością i symbolami funkcyjnymi
11. Rozstrzygalne klasy w logice klasycznej z równością i symbolami funkcyjnymi, mające własność modelu skończonego
12. Rozstrzygalne klasy w logice klasycznej z równością i symbolami funkcyjnymi, nie mające własności modelu skończonego
13. Logika intuicjonistyczna z symbolami funkcyjnymi i równością
Rodzaj przedmiotu
Tryb prowadzenia
Wymagania (lista przedmiotów)
Założenia (lista przedmiotów)
Koordynatorzy przedmiotu
Efekty kształcenia
Wiedza
K_W01 w pogłębionym stopniu - wiedzę z działów matematyki niezbędnych do studiowania informatyki (logika i jej związki z informatyką, teoria złożoności)
K_W02 w pogłębionym stopniu - rolę i znaczenie konstrukcji rozumowań matematycznych
Umiejętności
K_U01 konstruować rozumowania matematyczne
K_U02 wyrażać problemy obliczeniowe w języku matematyki
K_U04 projektować algorytmy w podstawowych modelach obliczalności: maszynach Turinga, obwodach logicznych
K_U05 identyfikować przynależność i trudność wybranych problemów obliczeniowych w stosunku do ważnych klas złożoności, wykorzystując ich różne charakteryzacje
K_U07 analizować pojęcia sformalizowane w wybranych systemach logicznych o znaczeniu informatycznym, tworzyć w nich formalizacje zadanych pojęć bądź też dowodzić niemożności takiej formalizacji
K_U10 samodzielnie planować i realizować własne uczenia się przez całe życie i ukierunkowywać innych w tym zakresie
K_U12 formułować i testować hipotezy związane z prostymi problemami badawczymi
Kompetencje społeczne
K_K01 krytycznej oceny posiadanej wiedzy i odbieranych treści
K_K02 uznawania znaczenia wiedzy w rozwiązywaniu problemów poznawczych i praktycznych oraz zasięgania opinii ekspertów w przypadku trudności z samodzielnym rozwiązaniem problemu
K_K03 myślenia i działania w sposób przedsiębiorczy
Kryteria oceniania
* Prace domowe 30%, egzamin 70%
* Dla doktorantów: badawcza praca domowa 50%, egzamin 50%
Literatura
* Egon Börger, Erich Grädel, Yuri Gurevich: The Classical Decision Problem. Perspectives in Mathematical Logic, Springer 1997
* M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006.
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
- Informatyka, stacjonarne, pierwszego stopnia
- Informatyka, stacjonarne, drugiego stopnia
- Matematyka, stacjonarne, drugiego stopnia
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: