A Generalization of Shostak#x2019;s Method for Combining Decision Procedures
Consider the problem of determining whether a quantifier-free formula ϕ is satisfiable in some first-order theory T . Shostak#x2019;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#x2019;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#x2019;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.
Unable to display preview. Download preview PDF.
- 2.C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In 17th International Conference on Automated Deduction, Lecture Notes in Computer Science. Springer-Verlag, 2000.Google Scholar
- 3.Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002.Google Scholar
- 4.Nikolaj S. Bjørner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999.Google Scholar
- 5.D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak’s Decision Procedure for Combinations of Theories. In M. McRobbie and J. Slaney, eds., 13th International Conference on Computer Aided Deduction, volume 1104 of Lecture Notes in Computer Science, pages 463–477. Springer-Verlag, 1996.Google Scholar
- 6.Z. Manna et al. STeP: Deductive-Algorithmic Verification of Reactive and Realtime Systems. In 8th International Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 415–418. Springer-Verlag, 1996.Google Scholar
- 7.Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999.Google Scholar
- 10.S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, ed., 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.Google Scholar
- 11.H. Ruess and N. Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19–28, June 2001.Google Scholar
- 13.C. Tinelli and M. Harandi. A New Correctness Proof of the Nelson-Oppen Combination Procedure. In F. Baader and K. Schulz, eds., 1st International Workshop on Frontiers of Combining Systems (FroCoS’96), volume 3 of Applied Logic Series. Kluwer Academic Publishers, 1996.Google Scholar
- 14.Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000.Google Scholar