NAIL062 Propositional and predicate logic: tutorial (Fall 2026)

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

Office hours during the teaching period

• Monday 6:50pm in N1 (Impakt)
• Thursday 2pm in front of S303 (on Oct 22 the start is postponed to 2:50pm)

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:

• 40 points for the SAT solver application project
• 10 points for activity during the tutorials

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 12 Sample test: Propositional Logic
• Predicate logic test date: Jan 7 Sample test: Predicate Logic

Retake test dates:

• propositional logic retake test: the first week of the examination period (date to be specified)
• predicate logic retake test: the first week of the examination period (date to be specified)

SAT solver application project

Read the following detailed project assignment carefully and follow all the instructions it contains. Submit your preferences in the specified format; otherwise, they will not be taken into account. The completed project must meet the stated requirements.

Deadlines:

• by Oct 25, submit your preferences (in the SIS Module Study Group Roster) and, if applicable, your own problem suggestion (via email)
• the project will be assigned shortly afterwards, also in the Study Group Roster
• by Nov 15, submit the link to your project repository (in the Study Group Roster)
• by the end of November, the repository must contain the completed project (with development progress clearly visible from commit history), no further changes will be taken into account
• during the first half of December, be prepared to demonstrate your project to the instructor if asked to do so

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

1st Tutorial (Oct 1)

• 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 8)

• Program: Continuation of the previous tutorial’s program.
• Materials: Continuing with worksheet1.pdf, solutions1.pdf

3rd Tutorial (Oct 15)

• 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

4th Tutorial (Oct 22)

• approaching the deadline for submitting preferences or sending suggestions for the SAT solver project
• 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

5th Tutorial (Oct 29)

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

6th Tutorial (Nov 5)

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

7th Tutorial (Nov 12)

• approaching the deadline to submit your SAT project repository link
• Propositional logic test
• Program: Introduction to predicate logic. Syntax and semantics of predicate logic.
• Materials: worksheet6.pdf, solutions6.pdf

8th Tutorial (Nov 19)

• approaching the deadline for submission of the SAT solver project
• Program: Syntax and semantics of predicate logic: continuation.
• Materials: (continuing with worksheet6.pdf)

9th Tutorial (Nov 26)

• approaching the deadline for submission of the SAT solver project
• Program: Structures and substructures. Extensions of theories. Extensions by definitions. Definable sets.
• Materials: worksheet7.pdf, solutions7.pdf

10th Tutorial (Dec 3)

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

11th Tutorial (Dec 10)

• Program: Conversion to PNF. Skolemization. Herbrand’s theorem. Unification. Demonstration of the resolution method.
• Materials: worksheet9.pdf, solutions9.pdf

12th Tutorial (Dec 17)

• Program: Resolution in predicate logic.
• Materials: worksheet10.pdf, solutions10.pdf

13th Tutorial (Jan 7)

• Predicate logic test
• Program: Selected advanced topics.
• 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.