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 language||English (US)|
|Number of pages||20|
|Journal||Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|
|State||Published - 2000|
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)