Deciding Combinations of Theories

Abstract

A method is given for decidlng formulas in combinations of unquantified first-order theories. Rather than couphng separate decision procedures for the contributing theories, the method makes use of a single, uniform procedure that minimizes the code needed to accommodate each additional theory. It is apphcable 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 anthmeUc, 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 underhes its completeness are also given. The procedure has been used extensively as the deductive core of a system for program specificaUon and verifcation. © 1984, ACM. All rights reserved.