@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",

}