A generalization of shostak’s method for combining decision procedures

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

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

Abstract

Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

Original languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings
PublisherSpringer Verlag
Pages132-146
Number of pages15
Volume2309
ISBN (Print)3540433813, 9783540433811
StatePublished - 2002
Event4th International Workshop on Frontiers of Combining Systems, FroCoS 2002 - Santa Margherita Ligure, Italy
Duration: Apr 8 2002Apr 10 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2309
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other4th International Workshop on Frontiers of Combining Systems, FroCoS 2002
CountryItaly
CitySanta Margherita Ligure
Period4/8/024/10/02

Fingerprint

Decision Procedures
Set theory
Generalization
First-order
Subset

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Barrett, C. W., Dill, D. L., & Stump, A. (2002). A generalization of shostak’s method for combining decision procedures. In Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings (Vol. 2309, pp. 132-146). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2309). Springer Verlag.

A generalization of shostak’s method for combining decision procedures. / Barrett, Clark W.; Dill, David L.; Stump, Aaron.

Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings. Vol. 2309 Springer Verlag, 2002. p. 132-146 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2309).

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

Barrett, CW, Dill, DL & Stump, A 2002, A generalization of shostak’s method for combining decision procedures. in Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings. vol. 2309, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2309, Springer Verlag, pp. 132-146, 4th International Workshop on Frontiers of Combining Systems, FroCoS 2002, Santa Margherita Ligure, Italy, 4/8/02.
Barrett CW, Dill DL, Stump A. A generalization of shostak’s method for combining decision procedures. In Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings. Vol. 2309. Springer Verlag. 2002. p. 132-146. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Barrett, Clark W. ; Dill, David L. ; Stump, Aaron. / A generalization of shostak’s method for combining decision procedures. Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings. Vol. 2309 Springer Verlag, 2002. pp. 132-146 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9ecf8849a5ec4d75b2385cde76e5f397,
title = "A generalization of shostak’s method for combining decision procedures",
abstract = "Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.",
author = "Barrett, {Clark W.} and Dill, {David L.} and Aaron Stump",
year = "2002",
language = "English (US)",
isbn = "3540433813",
volume = "2309",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "132--146",
booktitle = "Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings",

}

TY - GEN

T1 - A generalization of shostak’s method for combining decision procedures

AU - Barrett, Clark W.

AU - Dill, David L.

AU - Stump, Aaron

PY - 2002

Y1 - 2002

N2 - Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

AB - Consider the problem of determining whether a quantifierfree formula φ is satisfiable in some first-order theory T. Shostak’s algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak’s method. The first is a simple subset of Shostak’s algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak’s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak’s method based on a variation of the Nelson- Oppen method for combining theories.

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

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

M3 - Conference contribution

SN - 3540433813

SN - 9783540433811

VL - 2309

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 132

EP - 146

BT - Frontiers of Combining Systems - 4th International Workshop, FroCoS 2002, Proceedings

PB - Springer Verlag

ER -