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 2032.
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 (15% each, total 30%)
- Group lecture (total 45%): a lesson plan (15%) and the lecture itself (30%)
- 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
- Apr. 4: Due to inclement weather, the lecture is cancelled today. An email will be sent out later today with information on how today’s scheduled group lecture will be delivered.
- Mar. 23: Lecture notes for the ninth week have been posted.
- Mar. 16: Lecture notes for the eighth week have been posted.
- Mar. 9: Lecture notes for the seventh week have been posted.
- Mar. 7: The second assignment has been posted. It is due by Mar. 25 at 11:15am.
- Mar. 2: Lecture notes for the sixth week have been posted.
- Feb. 18: Information about the group lecture/report assessments has been posted.
- Feb. 16: Lecture notes for the fifth week have been posted.
- Feb. 9: Due to the impact of the cancelled lecture last week, the due date for Assignment 1 will be extended by five days. Assignment 1 is now due by Feb. 16 at 12:15pm.
- Feb. 7: Lecture notes for the fourth week have been posted.
- Feb. 4: Due to inclement weather, the lecture is cancelled today.
- Jan. 31: Lecture notes for the third week have been posted.
- Jan. 25: The first assignment has been posted. It is due by Feb. 11 at 11:15am.
- Jan. 24: Lecture notes for the second week have been posted.
- Jan. 17: Lecture notes for the first week have been posted.
- Jan. 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 |
| — | Winter study break | — |
| 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 |
| 10 | Group lectures | — |
| 11 | Group lectures | — |
| 12 | Group lectures | — |
Assignments
- Assignment 1, due
Feb. 11Feb. 16 - Assignment 2, due Mar. 25
- Group Lecture, due date varies
- Individual Report, due Apr. 13
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.
Personnel
Instructor
Taylor J. Smith
Email: tjsmith [at] stfx [dot] ca
Office: Annex, Room 9A
Student hours: Thursday, 9:15am–11:15am