Logic Summer School 2009 - Automated Theorem Proving

A course at the Summer Schools in Logic and Learning, Canberra, January, 2009.

Lecturer: Peter Baumgartner

Additional Information

• Slides and (superset of) the hand-written notes and proofs presented on whiteboard
• Example problems discussed in the lectures, see the files for more information how to run them:
  • Three-coloring problem instance (unsatisfiable)
  • Three-coloring problem instance (satisfiable)
  • Three-coloring problem - (dis)prove of functional dependency
  • Symmetries in the N-Queens problem
  • Disprove "all groups are abelian"

  The above problems are written in the widely TPTP-syntax. TPTP (Thousands of Problems for Theorem Proving) is a collection of test problems for automated theorem proving.

• Further reading
  • Wikipedia article on Automated Theorem Proving
  • For applications of Automated Theorem Proving see here.
  • Wikipedia article on Satisfiability Modulo Theories (SMT)
• The above pages contain a lot of links to theorem proving software.
  • Prover9 comes with a comprehensive set of examples and documentation. A good choice to start with.
  • Running the above example problems requires Darwin, E-Darwin (very experimental system) or Paradox (to disprove "all groups are abelian").