## 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

- Jan. 27: Lecture notes for the fourth week have been posted.
- 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 office 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 |

## 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