Completeness results for inequality provers (Q1079960)

This paper appears to be a free continuation of a previous paper by \textit{W. W. Bledsoe} and \textit{L. M. Hines} [Lect. Notes Comput. Sci. 87, 70-87 (1980; Zbl 0438.68050)], where a system of automated deduction, based on resolution, had been defined to discover proofs of propositions about dense total orders without endpoints. In particular, the system had been used to prove theorems about elementary calculus which involve the ordering of the real numbers. The present paper offers a precise formulation for this system and proves a completeness theorem for it. In this system, the order axioms are never stated explicitly, as they are entirely replaced by proof rules, e.g. the rule of chaining. Changing the inference rules, however, requires that certain other basic concepts of resolution be modified. Thus, two instances of substitution are allowed in the present paper, in order to decrease the length of a clause: self- chaining and factoring. The ground case for a set of clauses is defined and the completeness theorem is proved. Some suitable examples are involved to illustrate the main points of the theory.