A Framework for Cooperating Decision Procedures

Abstract. We present a exible framework for cooperating decision pro-cedures. We describe the properties needed to ensure correctness and show how it can be applied to implement an ecient version of Nel-son and Oppen's algorithm for combining decision procedures. We also show how a Shostak style decision procedure can be implemented in the framework in such a way that it can be integrated with the Nelson-Oppen method.