NAIL062 Propositional and predicate logic: tutorial (Fall 2025)

Here you will find information about the English tutorial class taught by me.

Office hours during the teaching period:

• Monday 10:40 in S303
• Monday 15:30 (after the lecture) in front of N1
• Thursday 14:00 in S303

or make an appointment (via email); two additional hours per week will be available.

Credit requirements

During the semester, there will be two written tests (45 minutes each). The first (roughly in the middle of the semester) will cover “Propositional Logic”, and the second (towards the end of the semester) will cover “Predicate Logic”. Each test is worth a maximum of 100 points. You will have one retake attempt for each test. No further retake opportunities will be provided.

In addition to the tests, up to 50 points can be earned from homework:

• 40 points for the SAT solver application project
• 5 points for propositional logic homework
• 5 points for predicate logic homework

Communication with anyone other than the instructor about the assignments is prohibited until the submission deadline. Solutions must be 100% your own work, and it is your responsibility to ensure that no one else has access to your solution.

To pass the course, you must earn at least 140 points in total, and at the same time at least 40 points from each test.

The written tests

• Propositional logic test date: TBA Sample test: Propositional Logic
• Predicate logic test date: TBA Sample test: Predicate Logic
• Preliminary retake dates (for both tests): during the first week of the exam period (will be specified depending on the number of students who will not have passed)

Homework

• Propositional logic homework: due TBA at the start of the exercise session. Task: solve the Sample test for propositional logic (Submit on paper or by email as a single PDF file with a white background.)
• Predicate logic homework: due TBA at the start of the exercise session. Task: solve the Sample test for predicate logic (Submit on paper or by email as a single PDF file with a white background. Part (c) of the first problem will not be graded, as we likely will not have enough time to practice it. However, it is recommended to try solving it.)
• SAT solver application project: detailed assignment, by TBA submit your preferences and issues, by TBA submit the finished project

Worksheets

1. Intro to propositional logic	worksheet1.pdf	solutions1.pdf
2. Semantics, properties of theories	worksheet2.pdf	solutions2.pdf
3. Algebra of propositions, SAT	worksheet3.pdf	solutions3.pdf
4. The tableaux method	worksheet4.pdf	solutions4.pdf
5. The resolution method	worksheet5.pdf	solutions5.pdf
6. Basics of predicate logic	worksheet6.pdf	solutions6.pdf
7. Properties of structures and theories	worksheet7.pdf	solutions7.pdf
8. The tableau method in predicate logic	worksheet8.pdf	solutions8.pdf
9. Prep for resolution in predicate logic	worksheet9.pdf	solutions9.pdf
10. Resolution in predicate logic	worksheet10.pdf	solutions10.pdf

Tutorial schedule (will be updated)

TBA

Program cvičení (bude aktualizováno)

1. cvičení (3. 10.)

• Program: Úvod do výrokové logiky. Základy syntaxe a sémantiky výrokové logiky. Ukázka tablo metody a rezoluční metody.
• Materiály: worksheet1.pdf, solutions1.pdf

2. cvičení (10. 10.)

• Program: Syntaxe a sémantika výrokové logiky. Univerzálnost logických spojek. Převod do CNF a DNF. Vlastnosti a extenze teorií.
• Materiály: worksheet2.pdf, solutions2.pdf

3. cvičení (17. 10.)

• Program: Počítání výroků až na ekvivalenci. 2-SAT a implikační graf. Horn-SAT a jednotková propagace. Algoritmus DPLL. Kódování problémů do SAT.
• Materiály: worksheet3.pdf, solutions3.pdf, ukázka SAT solveru včetně řešiče Glucose, viz také ukázka použití SAT solveru na řešení Sliding Puzzle

4. cvičení (24. 10.)

• Program: Tablo metoda ve výrokové logice. Věta o kompaktnosti a její aplikace.
• Materiály: worksheet4.pdf, solutions4.pdf

5. cvičení (31. 10.)

• Program: (pokračujeme v programu předchozího cvičení, řešíme nedodělané příklady)
• Materiály: (pokračujeme v worksheet4.pdf)

6. cvičení (7. 11.)

• Program: Rezoluce ve výrokové logice.
• Materiály: worksheet5.pdf, solutions5.pdf

7. cvičení (14. 11.)

• Termín odevzdání Domácího úkolu z výrokové logiky
• Program: Úvod do predikátové logiky. Syntaxe a sémantika predikátové logiky.
• Materiály: worksheet6.pdf, solutions6.pdf

8. cvičení (21. 11.)

• Zápočtový test z výrokové logiky
• Program: (pokračujeme v programu předchozího cvičení, řešíme nedodělané příklady)
• Materiály: (pokračujeme v worksheet6.pdf)

9. cvičení (28. 11.)

• blíží termín odevzdání projektu na SAT solver
• Program: Struktury a podstruktury. Extenze teorií. Extenze o definice. Definovatelné množiny.
• Materiály: worksheet7.pdf, solutions7.pdf

10. cvičení (5. 12.)

• Program: Tablo metoda v predikátové logice, jazyky s rovností. Aplikace Věty o kompaktnosti.
• Materiály: worksheet8.pdf, solutions8.pdf

11. cvičení (12. 12.)

• Program: Převod do PNF. Skolemizace. Herbrandova věta. Unifikace.
• Materiály: worksheet9.pdf, solutions9.pdf

12. cvičení (19. 12.)

• Termín odevzdání Domácího úkolu z predikátové logiky
• Program: Rezoluce v predikátové logice.
• Materiály: worksheet10.pdf, solutions10.pdf

13. cvičení (9. 1.)

• Zápočtový test z predikátové logiky
• Program: Vybraná témata z teorie modelů.
• Materiály: (pokračujeme v worksheet10.pdf)

–>

Useful Links

• The lecture and tutorial by Dr. Gregor
• Lecture notes by me
• Older lecture notes by Dr. Pilát

Frequently Asked Questions

• What should I do if I have a question about the exercises? — Check here in the FAQ section. If you don’t find an answer, email me; please include “nail062” and “tutorial” in the subject line.
• What should I do if I want a consultation? — Talk to me after class, come during the scheduled office hours, or set up an appointment via email.