Stephan Schulz: Implementation of First-Order Theorem Provers

First-order logic is in the Goldilocks Zone of deduction - expressive
enough to easily specify even complex properties, but simple enough to
support effective automatization. In this lecture, we will discuss the
implementation of efficient theorem proving systems for first-order
logic with equality.

After a short discussion of the logic and the calculus, the lecture
will cover the basic structure of a modern first-order theorem prover
based on clausification and saturation with redundancy elimination.
We will discuss the representation of the search state, the basic
saturation algorithm, search heuristics, and efficient algorithms and
data structures for implementing the most important operations. A
particular focus will be on proof search and on the implementation of
practically important simplification techniques.