Výroková a predikátová logika > Výroková a predikátová logika

Výroková a predikátová logika

Published on 28. září 2016 21:37

Požadavky na zápočet

Během semestru budeme psát dva testy (jeden na výrokovou a jeden na predikátovou logiku). Za každý z testů bude možné získat 10 bodů. Kromě toho také dostanete 3 domácí úkoly, každý za 2 body. Pro získání zápočtu je potřeba mít alespoň 16 bodů na konci semestru. Zápočet potřebujete před zkouškou.

Domácí úkoly

  1. k-obarvitelnost a SAT - termín 23. října 2019 večer, detaily jsou v přiloženém zipu
  2. výroková logika - termín 10. listopadu 2019 večer, detaily v pdf
  3. predikátová logika - termín 17. prosince 2019 večer, detaily v pdf

Testy

Test na výrokovou logiku se bude psát na cvičení 20. 11. 2019. Témata odpovídají tomu, co jsme zatím probrali:
- vyjadřování formulemi různých řádů (umět text zapsaný v přirozeném jazyce zapsat formálně v logice)
- normální tvary výroků - CNF, DNF (jak tabulkou tak syntakticky)
- implikační graf, jednotková propagace (řešení 2-SAT a HornSAT)
- tablo metoda
- počítání neekvivalentních výroků/teorií, které splňují zadanou podmínku
- rezoluční metoda

Test na predikátovou logiku budeme psát na cvičení 8. 1. 2020. Témata se budou týkat toho, co jsme procvičili z predikátové logiky:
- sémantika PL - struktury, podstruktury, ...
- teorie v PL, extenze a konzervativní extenze, modely teorií
- definovatelnost
- tablo metoda v PL
- převody na prenexní tvar, Skolemova varianta
- z rezoluce jen převod na množinovou reprezentaci a unifikace

Příklady ze cvičení

Na cvičení budeme používat především příklady z webu cvičení Petra Gregora. Odkazy na příklady níže se týkají právě jich.

Datum Téma
2. 10. 2019 Úvod, syntaxe vs sémantika, velikosti množin, výrokové formule, formule v jazyce prvního řádu a jazycích vyšších řádů (příklady 1.cv - 1, 2a, 2b)
9. 10. 2019 Převod formulí do CNF/DNF, splnitelnost, použití SAT řešičů (příklady 2. cv - 9a), bipartitnost a SAT (viz příklad u 1. domácího úkolu))
16. 10. 2019 Použití SAT solverů, CNF/DNF, univerzálnost spojek, 2-SAT (příklady 2. cvičení - 1, 8, 9b, 12)
23. 10. 2019 HornSAT, sémantika vzhledem k teorím, počty neekvivalentních výroků (příklady 3. cvičení - 1, 2, 3, 4, 6ab)
30. 10. 2019 počítání výroků, tablo metoda ve výrokové logice (příklady 4. cvičení - 1cd, 2abe, 3ac, 4ac, 5)
6. 11. 2019 aplikace kompaktnosti, rezoluční metoda (příklady 5. cvičení - 1, 3, 4ac, 5b, 6)
13. 11. 2019 rezoluční metoda ve VL, úvod do predikátové logiky - varianty, substituovatelnost, platnost ve struktuře (příklady 6. cvičení - 1, 4-8)
20. 11. 2019 test na výrokovou logiku, jeho řešení, sémantika PL (2. příklad ze 7. cvičení)
27. 11. 2019 sémantika predikátové logiky, struktury a podstruktury (příklady 8. cvičení - 1,3,4,5,6)
4. 12. 2019 teorie, extenze, definovatelnost, tablo metoda (příklady 8. cvičení - 6, 7, 8 a 10. cvičení - 2 )
11. 12. 2019 tablo metoda, prenexní tvar, Skolemizace (příklady 10. cvičení - 4 a 11. cvičení - 3, 4, 5)
18. 12. 2019 řešení domácího úkolu, rezoluce v predikátové logice (příklady 12. cvičení - 5, 6, 7 a kousek 10)