A framework for cooperating decision procedures

Clark W. Barrett, David L. Dill, Aaron Stump

Research output: Contribution to journalArticlepeer-review


We present a flexible framework for cooperating decision pro- cedures. We describe the properties needed to ensure correctness and show how it can be applied to implement an effcient 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.

Original languageEnglish (US)
Pages (from-to)79-98
Number of pages20
JournalLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
VolumeLNAI 1831
StatePublished - 2000

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'A framework for cooperating decision procedures'. Together they form a unique fingerprint.

Cite this