15-815 Automated Theorem Proving

Fall 99
Frank Pfenning
MWF 10:30-11:20
WeH 5409 A (WeH 4601 first 2 weeks of classes)
12 Units

This course provides a thorough, hands-on introduction to automated theorem proving. It consists of a traditional lecture component and a joint project in which we will construct a theorem prover. The lecture component introduces the basic concepts and techniques of logic followed by successive refinement towards more efficient implementations. The basic theorem proving paradigms we plan to cover are tableaux and the inverse method, both of which are applicable to classical and non-classical logics. Time permitting we may also cover some aspects of equational and inductive reasoning.

What's New?

• The course is over. If you would like to use some of the material here for a course, please get in touch with me at fp@cs.

Class Material

• Schedule
• Assignments
• Projects
• Resources
• Handouts
• Overview
• Links

Course Information

• Lectures: MWF 10:30-11:50, WeH 5409 A (WeH 4601 the first two weeks).
• Prerequisites: Some exposure to ML would be helpful. Undergraduates should have taken 15-212/ML or 15-312.
  
• Textbook: None. Course notes will be handed out.
• Grading: Course grade will be based 25% on the weekly homework, 25% on the midterm and 50% on the project.
• Credit: 12 Units.
• Topics: Natural Deduction, Sequent Calculi, Unification, Tableaux, Inverse Method, Term Indexing, Subsumption, Ordered Resolution
• Home: http://www.cs.cmu.edu/~fp/courses/atp/
• Directory: /afs/cs/user/fp/courses/atp/
• More: Further information on theorem proving.

Teaching Staff