Handbook of Automated Reasoning

Chapter 7

Paramodulation-Based Theorem Proving

Robert Nieuwenhuis; Albert Rubio

Contents

1  About this chapter    373

1.1  Paramodulation    373

1.2  Extending the unit equality case: ordered paramodulation    374

1.3  Redundancy and saturation    376

1.4  Computing with finite saturated sets    377

1.5  Paramodulation with constrained clauses    377

1.6  Paramodulation with built-in equational theories    379

1.7  Basic paramodulation with built-in equational theories    380

2  Preliminaries    380

2.1  Terms and (rewrite) relations    381

2.2  Term orderings    382

2.3  Equality clauses and Herbrand interpretations    384

2.4  Constraints and constrained clauses    385

3  Paramodulation calculi    385

3.1  The model ...