COMP 426: Automated Reasoning

The course will follow to a large extent the course notes from Frank Pfenning on Constructive Logic(CL) and on Automated Theorem proving(ATP). Both course notes are available in pdf-format.

- A nice high-level summary and background to this course can be found in the article "Proofs are Programs: 19th Century Logic and 21st Century Computing", Phil Wadler, which appeared in Dr Dobbs Journal, special supplement on Software in the 21st century, December 2000.
- What in the name of Euclid is going on here?, Science
- Proof and Beauty, Economist, Mar 31, 2005
- The QED Manifesto, appeared in "Automated Deduction - CADE 12", Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994.
- Wolfgang Thomas: Logic for Computer Science:The Engineering Challenge
- J. Halpern, R. Harper, N. Immerman, P. Kolaitis, M. Y. Vardi, V. Vianu: On the Unusual effectiveness of Logic in Computer Science
- NSF/CISE Workshop on The Unusual Effectiveness of Logic in Computer Science, National Science Foundation, 2001
- Michael Huth, Logic in Computer Science:tool-based modeling and reasoning about systems,Proceedings of the International Conference on Frontiers in Education 2000, Kansas City, October 2000.

- Model solution for HW5
- All homeworks and solutions are under Assignments
- Some induction examples in Tutch ind.tut
- Model solution for HW4

q1 and q2, q3 - Homework 5 is out

(pdf, ps, ass05.req) - Model solution are available

HW1 sol,

HW2 sol,

HW3-proof, HW3-part 2 - Homework 4 is out

(pdf, ps, ass04.tut) - Primitive recursion in Tutch (tut)
- Reading for the second half of the course are the notes on "Automated Theorem Proving".
- Reading for the first half of the course are the notes on "Constructive Logic".
- Slides on why studying automated reasoning and logic is interesting. (pdf)
- Schedule together with some general course information pdf and ps