A framework for cooperating decision procedures

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages79-98
Number of pages20
Volume1831
ISBN (Print)3540676643, 9783540676645
StatePublished - 2000
Event17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, United States
Duration: Jun 17 2000Jun 20 2000

Other

Other17th International Conference on Automated Deduction, CADE 2000
CountryUnited States
CityPittsburgh
Period6/17/006/20/00

Fingerprint

Decision Procedures
Correctness
Framework
Style

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Barrett, C. W., Dill, D. L., & Stump, A. (2000). A framework for cooperating decision procedures. In Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings (Vol. 1831, pp. 79-98). Springer Verlag.

A framework for cooperating decision procedures. / Barrett, Clark W.; Dill, David L.; Stump, Aaron.

Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Vol. 1831 Springer Verlag, 2000. p. 79-98.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Barrett, CW, Dill, DL & Stump, A 2000, A framework for cooperating decision procedures. in Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. vol. 1831, Springer Verlag, pp. 79-98, 17th International Conference on Automated Deduction, CADE 2000, Pittsburgh, United States, 6/17/00.
Barrett CW, Dill DL, Stump A. A framework for cooperating decision procedures. In Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Vol. 1831. Springer Verlag. 2000. p. 79-98
Barrett, Clark W. ; Dill, David L. ; Stump, Aaron. / A framework for cooperating decision procedures. Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings. Vol. 1831 Springer Verlag, 2000. pp. 79-98
@inproceedings{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",
language = "English (US)",
isbn = "3540676643",
volume = "1831",
pages = "79--98",
booktitle = "Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings",
publisher = "Springer Verlag",

}

TY - GEN

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

M3 - Conference contribution

SN - 3540676643

SN - 9783540676645

VL - 1831

SP - 79

EP - 98

BT - Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings

PB - Springer Verlag

ER -