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.

Material

• slides