Renamable paramodulation for automatic theorem proving with equality

摘要

Roughly speaking, in automatic theorem proving with equality, paramodulation is a substitution rule for equality. In this paper, renamable resolution is extended to paramodulation. Renamable paramodulation is paramodulation of two clauses which become positive after an R-renaming. We prove the R-refutation completeness of renamable resolution and renamable paramodulation for functionally reflexive systems. That is, we prove that, if a set S of clauses is R-unsatisfiable and if F is the set of the functionally reflexive axioms for S, then the empty clause can be derived from S & {x = x} & F using renamable resolution plus renamable paramodulation.