Deciding combinations of theories

Abstract

A method is given for deciding formulas in combinations of unquatified first-order theories. Rather than coupling separate decision procedures for the contributing theories, it makes use of a single, uniform procedure that minimizes the code needed to accommodate each additional theory. The method is applicable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that is closed under combination. Examples are given from the equational theories of integer and real arithmetic, a subtheory of monadic set theory, the theory of cons, car, and cdr, and others. A discussion of the speed performance of the procedure and a proof of the theorem that underlies its completeness are also given. The procedure has been used extensively as the deductive core of a system for program specification and verification.