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, 1:30pm–2:20pm; Wednesday, 12:30pm–1:20pm; Friday, 11:30am–12:20pm
All lectures are held in Mulroney Hall, room 4032.
Special Note for Winter 2024. On Monday, April 8, the Friday schedule of classes and labs will be offered.
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 25%): a lesson plan (10%) and the lecture itself (15%)
- Individual report on the group lecture (15%)
- 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
- Mar. 15: Lecture notes for the ninth week have been posted.
- Mar. 6: Lecture notes for the eighth week have been posted.
- Mar. 4: The second quiz will be written this week during the Mar. 8 lecture. See the Quizzes section below for more details.
- Mar. 1: Lecture notes for the seventh week have been posted. The second assignment has also been posted. It is due by Mar. 15 at 11:30am.
- Feb. 26: Information about the group lecture and report has been posted.
- Feb. 16: Lecture notes for the sixth week have been posted.
- Feb. 14: Due to the delayed opening of the university today, office hours this morning are cancelled.
- Feb. 9: Lecture notes for the fifth week have been posted.
- Feb. 4: Due to forecasted inclement weather, office hours and the lecture will be cancelled tomorrow.
- Jan. 31: Lecture notes for the fourth week have been posted.
- Jan. 29: The first quiz will be written this week during the Feb. 2 lecture. See the Quizzes section below for more details.
- Jan. 28: Due to forecasted inclement weather, office hours and the lecture will be cancelled tomorrow.
- Jan. 26: Lecture notes for the third week have been posted.
- Jan. 22: The first assignment has been posted. It is due by Feb. 9 at 11:30am.
- Jan. 19: Lecture notes for the second week have been posted.
- Jan. 12: Lecture notes for the first week have been posted.
- Jan. 10: Due to inclement weather, the lecture is cancelled today.
- Jan. 8: 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 |
| — | Winter study break | — |
| 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 |
| 10 | Group lectures | — |
| 11 | Group lectures | — |
| 12 | Group lectures | — |
Assignments
- Assignment 1, due Feb. 9
- Assignment 2, due Mar. 15
- Group Lecture, due date varies
- Individual Report, due Apr. 10
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: Feb. 2, 2023
Time: 11:30am–12:20pm
Place: Schwartz Hall, Room 156 (NOT our usual classroom)
Content: All material from Weeks 1 to 4
Quiz 2
Date: Mar. 8, 2023
Time: 11:30am–12:20pm
Place: Schwartz Hall, Room 156 (NOT our usual classroom)
Content: All material from Weeks 5 to 8
Personnel
Instructor
Taylor J. Smith
Email: tjsmith [at] stfx [dot] ca
Office: Annex, Room 9A
Office hours: Monday/Wednesday/Friday, 9:30am–10:30am