CSCI 544: Computational Logic (Winter 2024)

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

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

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

Assignments

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