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:40am in S303
• Monday 3:30pm (after the lecture) in front of N1
• Thursday 5:15pm 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. It is also not permitted to use generative AI tools when working on the assignment. 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: Nov 20 Sample test: Propositional Logic
• Predicate logic test date: Jan 8 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 Nov 13 at the beginning of class. Task: solve the Sample test for propositional logic (Submit on paper or in the SIS Module Study Group Roster as a single PDF file with white background.)
• Predicate logic homework: due Dec 18 at the start of the exercise session. Task: solve the Sample test for predicate logic (Submit on paper or in the SIS Module Study Group Roster as a single PDF file with 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 Oct 25 submit your preferences and suggestions for problems (in the SIS Module Study Group Roster), by end of November submit the finished project (in the SIS Module Study Group Roster)

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 tableau 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)

1st Tutorial (Oct 2)

• Program: Introduction to propositional logic. Basics of syntax and semantics of propositional logic. Demonstration of the tableau method and the resolution method.
• Materials: worksheet1.pdf, solutions1.pdf

2nd Tutorial (Oct 9)

• Program: Syntax and semantics of propositional logic. Universality of logical connectives. Conversion to CNF and DNF. Properties and extensions of theories.
• Materials: worksheet2.pdf, solutions2.pdf

3rd Tutorial (Oct 16)

• Program: Counting formulas up to equivalence. 2-SAT and implication graph. Horn-SAT and unit propagation. The DPLL algorithm. Encoding problems into SAT.
• Materials: worksheet3.pdf, solutions3.pdf, SAT solver example including the solver Glucose, see also example of using a SAT solver on the Sliding Puzzle

4th Tutorial (Oct 23)

• Program: Tableau method in propositional logic. The Compactness Theorem and its applications.
• Materials: worksheet4.pdf, solutions4.pdf

5th Tutorial (Oct 30)

• Program: (continuation of the previous tutorial’s program, finishing unfinished exercises) + light introduction to the resolution method
• Materials: (continuing with worksheet4.pdf)

6th Tutorial (Nov 6)

• Program: Resolution in propositional logic.
• Materials: worksheet5.pdf, solutions5.pdf

7th Tutorial (Nov 13)

• Deadline for submission of the homework on propositional logic
• Program: Introduction to predicate logic. Syntax and semantics of predicate logic.
• Materials: worksheet6.pdf, solutions6.pdf

8th Tutorial (Nov 20)

• Test on propositional logic
• approaching the deadline for submission of the SAT solver project
• Program: (continuation of the previous tutorial’s program, finishing unfinished exercises)
• Materials: (continuing with worksheet6.pdf)

9th Tutorial (Nov 27)

• Program: Structures and substructures. Extensions of theories. Extensions by definitions. Definable sets.
• Materials: worksheet7.pdf, solutions7.pdf

10th Tutorial (Dec 4)

• Program: Tableau method in predicate logic, languages with equality. Applications of the Compactness Theorem.
• Materials: worksheet8.pdf, solutions8.pdf

11th Tutorial (Dec 11)

• Program: Conversion to PNF. Skolemization. Herbrand’s theorem. Unification. Resolution in predicate logic.
• Materials: worksheet9.pdf, solutions9.pdf, worksheet10.pdf, solutions10.pdf

12th Tutorial (Dec 18)

• Deadline for submission of the homework on predicate logic
• Program: Resolution in predicate logic.
• Materials: worksheet10.pdf, solutions10.pdf

13th Tutorial (Jan 8)

• Test on predicate logic
• Program: Selected topics from model theory.
• Materials: (continuing with 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.