Skip to main content
SpringerLink
Log in

Shostak Light

  • Conference paper
  • First Online:
Automated Deduction—CADE-18 (CADE 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2392))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • 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 

  • 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.

    Chapter  Google Scholar 

  • Bachmair, L., Tiwari, A. & Vigneron, L. (2002), ‘Abstract congruence closure’, J. Automated Reasoning. To appear.

    Google Scholar 

  • 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

  • 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 

  • Bjørner, N. (1998), Integrating decision procedures for temporal verification, PhD thesis, Stanford University.

    Google Scholar 

  • Huet, G. (1972), Constrained Resolution: A Complete Method for Higher Order Logic, PhD thesis, Case Western Reserve University.

    Google Scholar 

  • 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 

  • Kapur, D. (2002), A rewrite rule based framework for combining decision procedures, in ‘Proc. FroCos 2002’, Springer-Verlag. to appear.

    Google Scholar 

  • 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 

  • Nelson, G. & Oppen, D. C. (1979), ‘Simplification by cooperating decision procedures’, ACM Transactions on Programming Languages and Systems 2(2), 245–257.

    Article  Google Scholar 

  • Nieuwenhuis, R. & Rubio, A. (1995), ‘Theorem proving with ordering and equality constrained clauses’, J. Symbolic Computation 19(4), 321–352.

    Article  MATH  MathSciNet  Google Scholar 

  • 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 

  • 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 

  • Shankar, N. & Rueß, H. (2002), Combining Shostak theories, in ‘Proc. RTA 2002’, Lecture Notes in Computer Science, Springer-Verlag. to appear.

    Google Scholar 

  • Shostak, R. E. (1984), ‘Deciding combinations of theories’, J. Association for Computing Machinery 31(1), 1–12.

    MATH  MathSciNet  Google Scholar 

  • 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 

  • Tiwari, A. (2000), Decision procedures in automated deduction, PhD thesis, SUNY at Stony Brook.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MPI Informatik, D-66123, Saarbrücken, Germany

    Harald Ganzinger

Authors
  1. Harald Ganzinger
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Manchester, Oxford Rd, Manchester, M13 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ganzinger, H. (2002). Shostak Light. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-45620-1_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43931-8

  • Online ISBN: 978-3-540-45620-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation