3rd International School on Rewriting
21 – 26 July 2008, Obergurgl, Austria
Program – Tracks A & B – Resolution Theorem Proving
Automated theorem proving in first-order logic has a number of applications, such as software verification, hardware verification and semantic web. The fastest first-order theorem provers, such as Vampire, E and Waldmeister, are based on the calculus of resolution and superposition, which heavily uses notions and techniques developed in rewriting.
I will introduce the key notions theory of resolution and superposition including
- proof systems,
- calculus of resolution and paramodulation,
- selection functions,
- redundancy criteria,
Further, I will comment on how this theory is used in the design of first-order theorem provers, giving rise to such notions as saturation algorithms and simplifying and generating inferences.
The cornerstone of the theory of resolution and paramodulation is a completeness theorem based on a model construction technique. We will show that this construction implies several classical theorems of first-order logic, namely compactness, Herbrand’s theorem, and existence of a model that is a factor algebra of the term algebra.