Handbook of Automated Reasoning

Chapter 27

Combining Superposition, Sorts and Splitting

Christoph Weidenbach

Contents

1 What This Chapter is (not) About   1967

2 Foundations   1969

3 A First Simple Prover   1973

4 Inference and Reduction Rules   1981

4.1 Reduction Orderings   1981

4.2 Sorts   1984

4.3 Inference Rules   1987

4.4 Reduction Rules   1991

4.5 Splitting   1998

5 Global Design Decisions   2000

5.1 Main-Loop   2000

5.2 Proof Documentation/Checking   2005

5.3 Data Structures and Algorithms   2005

Bibliography   2008

A Links to Saturation Based Provers   2011

Index   2012

1 What This Chapter is (not) About

This article is about the implementation of first-order saturation based clausal theorem provers. At the heart of such an implementation is a first-order calculus. ...