Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets

Abstract

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.