Złożoność określania własności logicznych stwierdzeń

monograficzne

Języki, automaty i obliczenia 1000-214bJAO
Podstawy matematyki 1000-211bPM

Logika dla informatyków 1000-217bLOG
Złożoność obliczeniowa 1000-218bZO

w sali

Na wykładzie przedstawiony zostanie stan wiedzy dotyczący zależności między użytym słownikiem symboli (kwantyfikatory, spójniki logiczne, rodzaje relacji oraz symboli funkcyjnych) używanych w wypowiedzeniu a złożonością problemu spełnialności oraz problemu dowodliwości.

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ą

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

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

* Prace domowe 30%, egzamin 70%

* Dla doktorantów: badawcza praca domowa 50%, egzamin 50%