Rewrite Techniques in Theorem Proving

Leo Bachmair SUNY at Stony Brook Harald Ganzinger MPI Saarbrücken

Tutorial CADE’94

Overview

The tutorial consist of three parts. Each describes a basic concept or technique of term rewriting and illustrates its application in first-order theorem proving.

1. Reduction orderings

2. Commutation and chaining

3. Redundancy and simplification