Automated Theorem Proving 2

Winter Semester 2010

First lecture on Fri 22 Oct 8:30 - 10:15 MZ 005 B

The course is a presentation of advanced techniques for automated reasoning: natural deduction, SAT, refinements of resolution, as well as of some practical implementation aspects of the Theorema system. The course is a continuation of Automated Theorem Proving 1, which is a prerequisite.

Lectures

• No lecture on Oct 8 and Oct 15, individual work:
  • Study the formalization of the propositional prover of Theorema.
  • Refresh the first part of the lecture (ATP 1) - see Books-ATP2.zip

• Oct. 22: Lecture 1:
  • The formalization of the Theorema propositional prover.