# 3rd International School on Rewriting

## 21 – 26 July 2008, Obergurgl, Austria

### Program – Tracks A & B – Resolution Theorem Proving

#### Lecturer

Andrei Voronkov#### Introduction

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,
- saturation,
- fairness,
- orderings,
- redundancy criteria,
- completeness.

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.