Contents may differ from the current or most recent offering of the course.
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:15pm–2:05pm; Wednesday, 12:15pm–1:05pm; Friday, 11:15am–12:05pm
All lectures are held in Mulroney Hall, room 4032.
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
- Mar. 10: Lecture notes for the ninth week have been posted.
- Mar. 3: Lecture notes for the eighth week have been posted.
- Mar. 2: Due to the delayed opening of the university, the lecture tomorrow is cancelled.
- Feb. 27: The second quiz will be written this week during the Mar. 1 lecture. See the Quizzes section below for more details.
- Feb. 17: Lecture notes for the seventh week have been posted.
- Feb. 17: The second assignment has been posted. It is due by Mar. 10 at 11:15am.
- Feb. 10: Lecture notes for the sixth week have been posted.
- Feb. 6: Information about the group lecture/report assessments has been posted.
- Feb. 3: Lecture notes for the fifth week have been posted.
- Jan. 27: Lecture notes for the fourth week have been posted.
- Jan. 23: The first quiz will be written this week during the Jan. 25 lecture. See the Quizzes section below for more details.
- Jan. 20: Lecture notes for the third week have been posted.
- Jan. 16: The first assignment has been posted. It is due by Feb. 3 at 11:15am.
- Jan. 16: Due to the delayed opening of the university, the student hour today is cancelled. The lecture today is still scheduled to be held as usual.
- Jan. 13: Lecture notes for the second week have been posted.
- Jan. 6: Lecture notes for the first week have been posted.
- Jan. 4: 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 |
| — | Winter study break | — |
| 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. 3
- Assignment 2, due Mar. 10
- Group Lecture, due date varies
- Individual Report, due Apr. 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: Jan. 25, 2023
Time: 12:15pm–1:05pm
Place: Mulroney Hall, Room 4032
Content: All material from Weeks 1 to 4
Quiz 2
Date: Mar. 1, 2023
Time: 12:15pm–1:05pm
Place: Mulroney Hall, Room 4032
Content: All material from Weeks 5 to 8
Personnel
Instructor
Taylor J. Smith
Email: tjsmith [at] stfx [dot] ca
Office: Annex, Room 9A
Student hours: Monday, 9:15am–11:15am