## Propositional and Predicate Logic - seminar

*Winter semester 2016/17*
**Schedule:** Wednesday 15:40-17:10, 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 -
*05. 10. 2016*: Statements expressed in formulae of various orders. HW: 5, 6.
- Seminar 2 -
*12. 10. 2016*: Adequacy, DNF and CNF. HW: 8, 9 a).
- Seminar 3 -
*19. 10. 2016*: 2-SAT and Horn-SAT, semantics in a theory, theories over finite languages. HW: 8b+c, 9a+d.
- Seminar 4 -
*26. 10. 2016*: Tableau method in propositional logic. HW: 7.
- Seminar 5 -
*02. 11. 2016*: Tableau method. Resolution method in propositional logic. HW: 11.
- Seminar 6 -
*09. 11. 2016*: Test 1. Resolution. Syntax of predicate logic. HW: 4, choose one of a), b), c).
- Seminar 7 -
*16. 11. 2016*: Syntax and semantics of predicate logic. HW: 6a+c).
- Seminar 8 -
*30. 11. 2016*: Semantics, substructures, theories, extensions. HW: 11.
- Seminar 9 -
*07. 12. 2016*: Tableau method in predicate logic. HW: 5.
- Seminar 10 -
*14. 12. 2016*: Prenex form, skolemization, extensions by definitions. HW: 8
- Seminar 11 -
*21. 12. 2016*: Herbrand's theorem, resolution. HW: 7
- Seminar 12 -
*04. 01. 2017*: Resolution in predicate logic.

**Announcement:** The second test will be on January 11.

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