Deciding Combinations of Theories

Abstract

A method ~s g~ven for dec~dlng 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 ~s apphcable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that ~s 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 ~ts completeness are also g~ven. The procedure has been used extensively as the deductive core of a system for program specificaUon and verifcation.