Handbook of Automated Reasoning

Chapter 10

Equality Reasoning in Sequent-Based Calculi

Anatoli Degtyarev; Andrei Voronkov

Contents

1  Introduction    613

1.1  Some useful notation    614

1.2  Equality. The first axiomatization    615

1.3  Paramodulation and its refinements    616

1.4  Equality in sequent systems    622

1.5  Overview of calculi introduced in this chapter    628

2  Translation of logic with equality into logic without equality    628

2.1  Modification method    630

2.2  Constrained equality elimination    633

3  Free variable systems    637

3.1  Free variable tableaux    637

3.2  Matings    640

3.3  The inverse method    641

4  Early history    644

5  Simultaneous rigid E-unification    646

5.1  Definition and examples    646

5.2