CSE533 Propositional Theorem Proving, Satisfiability Testing and Proof Complexity

General information

Instructor: Paul Beame
Meeting times: Tuesday, Thursday 12:00-1:20 in Loew 113.
Automated theorem proving and computer-aided verification in AI, VLSI, and Software Engineering give algorithms that attempt to decide the truth of logical statements in propositional or in first- (or higher-) order logic. This course will concentrate on complexity issues for the propositional case as well as for its flip side, satisfiability-testing. (Even the uses of theorem proving in first-order and higher-order logic often involve finite domains where the proofs can be interpreted in propositional logic anyway.)
We will consider a variety of systems for propositional theorem proving and satisfiability testing. Key issues for such systems are:
  • How complex are proofs within the system?
  • What are good choices for search strategies?
    • There has been considerable theoretical and practical work on both of these questions. We will concentrate on theoretical issues of proof complexity and of the relative complexity of search strategies. We will also examine a number of implementations of propositional logic algorithms to compare theory and practice.

    Papers and things

  • Urquhart's Complexity of Proofs Survey
  • 519 talk slides

    • Installed software

    For our amusement I have installed a few theorem provers, ANL-DP, Sato, and Boyer Moore as well as one satisfiability tester, Gsat on june in the directory:
  • /cse/courses/cse533/provers
    • There are few papers scattered there as well and I am in the process of installing more theorem provers.