COMP 426 Automated Reasoning
Schedule

Lectures are Tuesday and Thursday at 11:35am - 12:55pm in the MacDonald Harrington Building, Room MMDHAR G-01.
The class notes provide additional reading material.
They complement, but do not replace the lecture.
The schedule is subject to change throughout the semester.

Date			Lecture or Recitation	Reading	Code

Thu	Sep	2	Overview	Slides

Tue	Sep	7	Natural Deduction	Ch 1 + 2 (ATP), Ch 2(CL)
Thu	Sep	9	Notational definitions

Tue	Sep	14	Proof terms	Ch2 (ATP), Ch 3(CL)
Thu	Sep	16	Proof terms - cont.		pchecker

Tue	Sep	21	Proof (Type) Checking
Thu	Sep	23	Intercalation	Ch. 3.1

Tue	Sep	28	Normal derivations	Ch. 3.1
Thu	Sep	30	Sequent Calculus	Ch. 3.3

Tue	Oct	5	Cut-elimination	Ch 3.4
Thu	Oct	7	Quantification	Ch1-3

Tue	Oct	12	Bi-directional proof checking	Ch 3.2, Ch 3.6
Thu	Oct	14	Inversion and Focusing	Ch 4.1

Tue	Oct	19	Midterm
Thu	Oct	21	Review: Midterm

Tue	Oct	26	Inversion-based search	Ch 4.1
Thu	Oct	28	Implementing focusing provers	Ch 4.1, Ch 4.3

Tue	Nov	2	Guided theorem proving
Thu	Nov	4	Horn Clauses	Ch 4.2

Tue	Nov	9	Unification (1)	Ch 4.4, 4.5
Thu	Nov	11	Unification (2)	Ch 4.4, 4.5

Tue	Nov	16	Hereditary Harrop Formulas		examples
Thu	Nov	18	Tabled logic programming

Tue	Nov	23	Higher-order abstract syntax
Thu	Nov	25	Linear logic (1)

Tue	Nov	30	Linear Logic (2)