ISR 2008

3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Tracks A & B – Resolution Theorem Proving


Andrei Voronkov


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

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.