Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
James Robert Slagle · Journal of the ACM · 1972
TO make further progress, resolution principle programs need to make better inferences and to make them faster.This paper presents a fairly general approach for taking some advantages of the structure of special theories, for example, the theories of equality, partial ordering, and sets.The object of the approach is to replace some of the axioms of a given theory by (refutation) complete, valid, efficient (in time) inference rules.The author believes that the new rules are efficient because: (1) inference for inference, a computer program embodying the rules should be faster than a resolution program computing with the corresponding axioms; (2) more importantly, certain troublesome inferences made by resolution are avoided by the new rules.In this paper, the three main applications of the approach concern "building-in" the theories of equality, partial ordering, and sets and may be stated roughly as follows.(1) If only {x =x} is retained from the equality axioms, and if the others are replaced by the functionally reflexive axioms and the rule of renamable paramodulation, refutation completeness is preserved.(2) If only {xC_x} is retained from the eight (not all independent) partial ordering axioms for { =, C:, C:} and if the other seven are replaced by the rules r(C::, C) and r(C:), refutation completeness is preserved.(3) If a certain seven of the twenty-four set axioms are retained and if the remaining seventeen are replaced by the rules r(C::, ~), r(C), r(C ), r(e) (complement), r( U ), r(['l ), and r(u) (unit sets), refutation completeness is preserved.