Superposition with equivalence reasoning and delayed clause normal form transformation
This paper describes a superposition calculus where quantifiers are eliminated lazily. Superposition and simplification inferences may employ equivalences that have arbitrary formulas at their smaller side. A closely related calculus is implemented in the Saturate system and has shown useful on many examples, in particular in set theory. The paper presents a completeness proof and reports on practical experience obtained with the Saturate system. (c) 2005 Published by Elsevier Inc.
superposition set theory automated theorem proving deduction rewriting clause-normal-form transformation logical equivalence paramodulation first-order logic