Advertisement

Shostak Light

  • Harald Ganzinger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

We represent the essential ingredients of Shostak’s procedure at a high level of abstraction, and as a refinement of the Nelson-Oppen procedure. We analyze completeness issues of the method based on a general notion of theories. We also formalize a notion of σ-models and show that on the basis of Shostak’s procedure we cannot distinguish a theory from its approximation represented by the class of its σ-models.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F. & Tinelli, C. (1997), A new approach for combining decision procedures for the word problem, and its connection to the nelson-oppen combination method, in W. McCune, ed., ‘Automated Deduction — CADE-14, 14th International Conference on Automated Deduction’, LNAI 1249, Springer-Verlag, Townsville, North Queensland, Australia, pp. 19–33.Google Scholar
  2. Bachmair, L. & Tiwari, A. (2000), Abstract congruence closure and specializations, in D. McAllester, ed., ‘Automated Deduction — CADE-17, 17th International Conference on Automated Deduction’, LNAI 1831, Springer-Verlag, Pittsburgh, PA, USA, pp. 64–78.CrossRefGoogle Scholar
  3. Bachmair, L., Tiwari, A. & Vigneron, L. (2002), ‘Abstract congruence closure’, J. Automated Reasoning. To appear.Google Scholar
  4. Barrett, C., Dill, D. & Levitt, J. (1996), Validity checking for combinations of theories with equality, in M. Srivas & A. Camilleri, eds, ‘Formal Methods In Computer-Aided Design, Palo Alto/CA, USA’, Vol. 1166, Springer-Verlag, pp. 187–201. http://cite-seer.nj.nec.com/barrett96validity.html
  5. Barrett, C., Dill, D. & Stump, A. (2002), A generalization of Shostak’s method for combining decision procedures, in ‘Proc. FroCos 2002’, Springer-Verlag. to appear.Google Scholar
  6. Bjørner, N. (1998), Integrating decision procedures for temporal verification, PhD thesis, Stanford University.Google Scholar
  7. Huet, G. (1972), Constrained Resolution: A Complete Method for Higher Order Logic, PhD thesis, Case Western Reserve University.Google Scholar
  8. Kapur, D. (1997), Shostak’s congruence closure as completion, in H. Comon, ed., ‘Rewriting Techniques and Applications’, Lecture Notes in Computer Science, Springer, Sitges, Spain, pp. 23–37.Google Scholar
  9. Kapur, D. (2002), A rewrite rule based framework for combining decision procedures, in ‘Proc. FroCos 2002’, Springer-Verlag. to appear.Google Scholar
  10. Manna, Z., Anuchitanulu, A., Bjørner, N., Browne, A., Chang, E. S., Colón, M., de Alfaro, L., Devarajan, H., Kapur, A., Lee, J., Sipma, H. & Uribe, T. E. (1995), STeP: The Stanford Temporal Prover, in ‘TAPSOFT’, Vol. 915 of Lecture Notes in Computer Science, Springer-Verlag, pp. 793–794.Google Scholar
  11. Nelson, G. & Oppen, D. C. (1979), ‘Simplification by cooperating decision procedures’, ACM Transactions on Programming Languages and Systems 2(2), 245–257.CrossRefGoogle Scholar
  12. Nieuwenhuis, R. & Rubio, A. (1995), ‘Theorem proving with ordering and equality constrained clauses’, J. Symbolic Computation 19(4), 321–352.zbMATHCrossRefMathSciNetGoogle Scholar
  13. Owre, S., Rushby, J. M. & Shankar, N. (1992), PVS: A prototype verification system, in D. Kapur, ed., ‘11th International Conference on Automated Deduction’, LNAI 607, Springer-Verlag, Saratoga Springs, New York, USA, pp. 748–752.Google Scholar
  14. Rueß, H. & Shankar, N. (2001), Deconstructing Shostak, in ‘Proceedings of the Sixteenth IEEE Symposium On Logic In Computer Science (LICS’01)’, IEEE Computer Society Press, pp. 19–28.Google Scholar
  15. Shankar, N. & Rueß, H. (2002), Combining Shostak theories, in ‘Proc. RTA 2002’, Lecture Notes in Computer Science, Springer-Verlag. to appear.Google Scholar
  16. Shostak, R. E. (1984), ‘Deciding combinations of theories’, J. Association for Computing Machinery 31(1), 1–12.zbMATHMathSciNetGoogle Scholar
  17. Tinelli, C. & Harandi, M. (1996), A new correctness proof of the Nelson-Oppen combination procedure, in ‘1st Int’l Workshop on Frontiers of Combining Systems (FroCoS’96)’, Vol. 3 of Applied Logic Series, Kluwer Academic Publishers.Google Scholar
  18. Tiwari, A. (2000), Decision procedures in automated deduction, PhD thesis, SUNY at Stony Brook.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Harald Ganzinger
    • 1
  1. 1.MPI InformatikSaarbrückenGermany

Personalised recommendations