@inproceedings{9ecf8849a5ec4d75b2385cde76e5f397,
title = "A generalization of shostak{\textquoteright}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{\textquoteright}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{\textquoteright}s method. The first is a simple subset of Shostak{\textquoteright}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{\textquoteright}s algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak{\textquoteright}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",
note = "4th International Workshop on Frontiers of Combining Systems, FroCoS 2002 ; Conference date: 08-04-2002 Through 10-04-2002",
}