A Framework of Refutational Theorem Proving for Saturation−Based Decision Procedures

Abstract

Automated state-of-the-art theorem provers are typically optimised for particular strategies, and there are only limited number of options that can be set by the user. Probably because of this, the general conditions on applicability of saturation-based calculi have not been thoroughly investigated. However for some applications, e.g., for saturation-based decision procedures, one would like to have more options in order to design flexible saturation strategies. In this report we revisit several well-known saturation-based calculi used in automated deduction: Ordered Resolution, Ordered Paramodulation, Superposition and Chaining calculi. We give a uniform account on completeness proofs for these calculi using the standard model construction procedures of Bachmair and Ganzinger. By careful inspection of these proofs, we formulate some variations of inference rules and general conditions on orderings under which the calculi remain refutationally complete. In particular, we considerably generalise the known class of admissible orderings for the Chaining calculi. We also consider in details the standard notion of redundancy, estimate the complexity for the steps of the clause normal form transformation, and give a computational model of the saturation process.