Handouts -- Fall 2007

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.

Supplementary material

• 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.

Handouts

• 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