## Propositional and Predicate Logic - seminar

*Winter semester 2014/15*
**Schedule:** Monday 17:20-18:50, room S11.

**Lecturer:** Petr Gregor (gregor(at)ktiml.mff.cuni.cz)

**Information on the lecture:** 2/2 Zk/Z NAIL062 in SIS, on the page of the lecture.

**Exercises**

- Seminar 1 -
*06. 10. 2014*: Statements expressed in formulae of various orders.
- Seminar 2 -
*13. 10. 2014*: Expressing statements in formulae cont., adequacy, DNF and CNF, semantics of propositional logic.
- Seminar 3 -
*20. 10. 2014*: 2-SAT and Horn-SAT, semantics in a theory.
- Seminar 4 -
*27. 10. 2014*: Analysis of theories with finite languages. Tableau method in propositional logic.
- Seminar 5 -
*03. 11. 2014*: Tableau method. Resolution method in propositional logic.
- Seminar 6 -
*10. 11. 2014*: Test 1. Resolution method.
- Seminar 7 -
*24. 11. 2014*: Basic syntax and semantics of predicate logic.
- Seminar 8 -
*01. 12. 2014*: Semantics of predicate logic, theories, substructures, open theories.
- Seminar 9 -
*08. 12. 2014*: Extensions of theories. Tableau method in predicate logic.
- Seminar 10 -
*15. 12. 2014*: Tableau method, compactness, prenex normal form.
- Seminar 11 -
*05. 01. 2015*: Test 2. Skolemisation, extensions by definitions, resolution via grounding.

**Credits**

There will be two tests throughout the semester. For the credit from the seminar you need to obtain at least 2/3 points for the tests. Additional points can be obtained for activity during the seminars or occasional homework.