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