Zadanie

Zadanie - 20 bodov

Zadanie pozostáva z viacerých kreatívnych úloh zameraných na overenie celkového pochopenia danej problematiky. Zadanie je možné rozdeliť do 3 tematických okruhov:

• Výroková logika.
• Predikátová logika.
• Ďalšie logické systémy.

Výroková logika

Vašou úlohou v rámci tejto časti zadania, bude vymyslieť vetu (alebo sylogizmus) v prirodzenom jazyku, ktorú prepíšete do formuly jazyka výrokovej logiky.

• Formula musí byť tautológia a bude obsahovať minimálne 4 výrokové premenné (elementárne výroky) a minimálne 5 logických spojok (z toho aspoň 4 binárne) a následne:
• Zostrojte strom abstraktnej syntaxe formuly.
• Vypočítajte veľkosť formuly.
• Vypočítajte množinu všetkých podformúl formuly.
• Pomocou tabuľky pravdivostných hodnôt overte, že formula je tautológia.
• Dokážte formulu pomocou naturálnej dedukcie.
• Dokážte formulu pomocou sekventového kalkulu.
• Dokážte formulu pomocou rezolučnej metódy.

Upravte navrhnutú vetu (sylogizmus) v prirodzenom jazyku tak aby bola splniteľná a zároveň nebola tautológia alebo kontradikcia.

• Preložte upravenú vetu do jazyka výrokovej logiky.
• Pomocou tabuľky pravdivostných hodnôt zistite, či upravená formula je splniteľná a zároveň:
• Zostrojte strom abstraktnej syntaxe formuly.
• Vypočítajte veľkosť formuly.
• Vypočítajte množinu všetkých podformúl formuly.
• Nájdite konjunktívny normálny tvar prostredníctvom naivného prepisu.
• Nájdite disjunktívny normálny tvar prostredníctvom naivného prepisu.
• Nájdite úplný konjunktívny normálny tvar.
• Nájdite úplný disjunktívny normálny tvar.
• Nájdite aspoň jeden minimálny konjunktívny normálny tvar.
• Nájdite aspoň jeden minimálny disjunktívny normálny tvar.
• Nájdite konjunktívny normálny tvar formuly pomocou Tseitinovej transformácie.
• Výsledné tvary formuly v konjunktívnom normálnom tvare prepíšte do množinovej notácie (všetky 4).
• Aplikujte algoritmus DPLL na množiny klauzúl (všetky 4) z predchádzajúceho bodu a nájdite model formuly.

Predikátová logika

Navrhnutú vetu resp. sylogizmus v prirodzenom jazyku (z prvej časti zadania) rozšírte o vlastnosti, ktoré je možné opísať predikátmi, funkčnými symbolmi a kvantifikátormi (resp. navrhnite novú).

• Prepíšte túto vetu do formuly jazyka predikátovej logiky.
• Dokážte formulu prirodzenou dedukciou.
• Dokážte formulu sekventovým kalkulom.
• Dokážte formulu rezolučnou metódou.

Prostredníctvom interaktívneho dokazovacieho systému OnlineProver dokážte aspoň 5 ľubovoľných formúl predikátovej logiky (úlohy example 10 a nižšie).

Napíšte program logickej paradigmy tak, že bude obsahovať aspoň:

• 10 faktov,
• 5 pravidiel.

Formulujte aspoň jeden cieľ (komplexný) a dokážte jeho platnosť/neplatnosť prostredníctvom SLD-rezolúcie.

Prepíšte Váš logický program do programovacieho jazyka logickej paradigmy a overte korektnosť Vášho riešenia.

Prepíšte Vašu formulu a logický program do formátu TPTP FOF a dokážte ju ľubovoľným príslušným automatickým dokazovacím systémom.

Neklasické logické systémy

Forma odovzdania

Termín pre odovzdanie finálnej verzie zadania je koniec 12. týždňa semestra v systéme moodle v kurze LPI.

Odovzdávanie zadania bude prebiehať priebežne, prostredníctvom systému moodle.

• Pre priebežné odovzdávky v 5. 9. a 12. týždni bude vytvorená aktivita na odovzdanie vypracovanej časti zadania.
• V danom týždni je potrebné vypracovať časť zadania, podľa obsahu cvičenia z predchádzajúcich týždňov.
• Zadanie nie je potrebné rozdeliť do viacerých projektov ale priebežne dopĺňať.
• V aktuálnej odovzdávke sú povolené zmeny aj v už odovzdaných častiach zadania. Neospravedlnené nedodržanie termínu odovzdávky bude sankcionované stratou 5 bodov.

Zadanie je možné vypracovať dvoma spôsobmi:

• Využitím typografického systému LaTeX (max. 20 bodov).
• Ručne s možnosťou získania max. 13 bodov.

Zadanie v úvodnej časti bude obsahovať:

• titulnú stranu,
• súhrn rozsahu vyriešených úloh (obsah).

Forma odovzdania:

• V prípade zvolenia 1. možnosti poprosím odovzdanie vypracovaného zadania spolu so zdrojovými kódmi. Spôsob vypracovania je voľný, t.j. môžete použiť ľubovoľné balíky typografického systému LaTeX pre vizualizáciu jednotlivých úloh.
• V prípade voľby 2. možnosti Vás poprosím o odovzdanie zadania vo forme jedného pdf súboru.

Obhajoba zadania bude prebiehať v 13. týždni.