Course Description
This course focuses on automated theorem proving. We start with a rigorous treatment of propositional and first order calculus and the method of natural deduction, giving a thorough investigation of the soundness and completeness proofs and decidability. Then we compare and contrast several automated theorem proving methods such as tableau, resolution, sequent style calculus and rewrite systems. Extensions to other logics will be discussed.
See the course outline for more information.
Course Details
Lecture Time/Place
Monday, 10:30am–11:20am; Wednesday, 9:30am–10:20am; Friday, 8:30am–9:20am
All lectures are held in Mulroney Hall, room 3024.
Textbook
M. Fitting, First-Order Logic and Automated Theorem Proving. Springer-Verlag, 2nd edition, 1996.
The textbook is not required, but is useful as a secondary reference. Course notes will also be provided for each lecture.
Marking Scheme
- Two assignments (10% each, total 20%)
- Two quizzes (15% each, total 30%)
- Group lecture (total 30%): a lesson plan (10%) and the lecture itself (20%)
- Individual report on the group lecture (10%)
- Participation (10%): class participation (5%) and reviewing group lectures (5%)
You must complete the group lecture and individual report components in order to pass the course. You may not complete one without completing the other.
News
- Dec. 5: Due to the delayed opening of the university today, the lecture this morning is cancelled.
- Nov. 3: Lecture notes for the ninth week have been posted.
- Oct. 27: The second quiz will be written this week during the Oct. 29 lecture. See the Quizzes section below for more details.
- Oct. 24: Lecture notes for the eighth week have been posted.
- Oct. 20: The second assignment has been posted. It is due by Nov. 5 at 9:30am.
- Oct. 20: Lecture notes for the seventh week have been posted.
- Oct. 15: The lecture on Friday will be cancelled due to the instructor being away.
- Oct. 10: Lecture notes for the sixth week have been posted.
- Oct. 8: Information about the group lecture and report has been posted.
- Oct. 6: The first quiz will be written this week during the Oct. 8 lecture. See the Quizzes section below for more details.
- Oct. 1: Lecture notes for the fifth week have been posted.
- Sep. 24: As mentioned in lecture today, the lectures on Friday and next Monday will be cancelled due to the instructor being away.
- Sep. 24: The first assignment has been posted. It is due by Oct. 15 at 9:30am.
- Sep. 22: Lecture notes for the fourth week have been posted.
- Sep. 15: Lecture notes for the third week have been posted.
- Sep. 8: Lecture notes for the second week have been posted.
- Sep. 3: Lecture notes for the first week have been posted.
- Sep. 3: Welcome to the course! Please see our Moodle page for details about the course this term.
Lectures
| Week | Notes | Readings |
| 1 | Introduction | Fitting, Ch. 1 |
| 2 | Propositional logic: syntax and semantics | Fitting, 2.1–2.5 |
| 3 | Propositional logic (cont’d): semantic tableaux | Fitting, 3.1–3.2, 3.4–3.7 |
| 4 | Propositional logic (cont’d): natural deduction | Fitting, 4.1–4.2 |
| 5 | Propositional logic (cont’d): resolution | Fitting, 3.3–3.4, 3.7 |
| 6 | Predicate logic: syntax and semantics | Fitting, 5.1–5.3 |
| 7 | Predicate logic (cont’d): semantic tableaux | Fitting, 6.1, 6.3–6.4 |
| 8 | Predicate logic (cont’d): natural deduction | Fitting, 6.5–6.6 |
| 9 | Predicate logic (cont’d): ground and general resolution | Fitting, 6.2, 6.3–6.4 |
| – | Fall study break | – |
| 10 | Group lectures | — |
| 11 | Group lectures | — |
| 12 | Group lectures | — |
Assignments
- Assignment 1, due Oct. 15
- Assignment 2, due Nov. 5
- Group Lecture, due date varies
- Individual Report, due Dec. 5
Assignments are due at the beginning of class on the due date. Late assignments will be accepted up to the beginning of the first class following the due date. Late assignments are subject to a penalty of 10% deducted from the earned mark.
The group lecture and individual report must be submitted on the due date. Late submissions will not be accepted.
Quizzes
Quiz 1
Date: Oct. 8, 2025
Time: 9:30am–10:20am
Place: Keating Centre, Room 1018A (NOT our usual classroom)
Content: All material from Weeks 1 to 4
Quiz 2
Date: Oct. 29, 2025
Time: 9:30am–10:20am
Place: Coady Hall, Room 120 (NOT our usual classroom)
Content: All material from Weeks 6 to 8
Personnel
Instructor
Taylor J. Smith
Email: tjsmith [at] stfx [dot] ca
Office: Annex, Room 9A
Office hours: Monday 11:30am–12:20pm/Wednesday 10:30am–11:20am/Friday 9:30am–10:20am, or by appointment