A Framework for Cooperating Decision Procedures

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

doi:10.1007/10721959_6

Back

A Framework for Cooperating Decision Procedures

Book chapter

Peer reviewed

A Framework for Cooperating Decision Procedures

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

Automated Deduction - CADE-17, pp.79-98

Lecture Notes in Computer Science, Springer Berlin Heidelberg

2000

DOI: 10.1007/10721959_6

View Online

Abstract

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

Atomic Formula

Consistent State

Decision Procedure

Directed Acyclic Graph

Oppen Theory

Details

Title: Subtitle: A Framework for Cooperating Decision Procedures
Creators: Clark W. Barrett - Stanford University
David L. Dill - Stanford University
Aaron Stump - Stanford University
Resource Type: Book chapter
Publication Details: Automated Deduction - CADE-17, pp.79-98
Publisher: Springer Berlin Heidelberg; Berlin, Heidelberg
Series: Lecture Notes in Computer Science
DOI: 10.1007/10721959_6
eISSN: 1611-3349
ISSN: 0302-9743
Language: English
Date published: 2000
Academic Unit: Computer Science
Record Identifier: 9984259405802771

Metrics

3 Record Views