A framework for cooperating decision procedures

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

doi:10.1007/10721959_6

A framework for cooperating decision procedures

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

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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)
Pages (from-to)	79-98
Number of pages	20
Journal	Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Volume	LNAI 1831
DOIs	https://doi.org/10.1007/10721959_6
State	Published - 2000

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/10721959_6

Cite this

@article{4f652a77757b4c14b963812cdb776ae3,

title = "A framework for cooperating decision procedures",

abstract = "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.",

author = "Barrett, {Clark W.} and Dill, {David L.} and Aaron Stump",

year = "2000",

doi = "10.1007/10721959_6",

language = "English (US)",

volume = "LNAI 1831",

pages = "79--98",

journal = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - A framework for cooperating decision procedures

AU - Barrett, Clark W.

AU - Dill, David L.

AU - Stump, Aaron

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84937440744&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84937440744&partnerID=8YFLogxK

U2 - 10.1007/10721959_6

DO - 10.1007/10721959_6

M3 - Article

AN - SCOPUS:84937440744

SN - 0302-9743

VL - LNAI 1831

SP - 79

EP - 98

JO - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)

JF - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)

ER -

A framework for cooperating decision procedures

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this