Advertisement

Adding external decision procedures to HOL90 securely

  • Elsa L. Gunter
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

This paper describes a modest conservative extension of HOL90 that allows the results from external decision procedures to be used within HOL90 without compromising its logical consistency.

Keywords

Model Check Inference Rule Decision Procedure Free Variable Computer Algebra System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. J. Boulton. A Lazy Approach to Fully-Expansive Theorem Proving. In Higher Order Logic Theorem Proving and Its Applications. North-Holland, 1992.Google Scholar
  2. 2.
    M. J. C. Gordon and T. Melham, Introduction to HOL. Cambridge University Press, 1993.Google Scholar
  3. 3.
    J. Harrison and L. Théry. Extending the HOL theorem prover with a Computer Algebra System to Reason about the Reals. In Higher Order Logic Theorem Proving and Its Applications. Springer-Verlag, 1993.Google Scholar
  4. 4.
    P. V. Homeier and D. F. Martin. A Mechanically Verified Verification Condition Generator. In The Computer Journal, Vol. 38, No. 2, July 1995, pages 131–141.CrossRefGoogle Scholar
  5. 5.
    G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall Software Series, 1991.Google Scholar
  6. 6.
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
  7. 7.
    S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In Proceedings of CAV'96, Lecture Notes in Computer Science. Springer Verlag, 1996.Google Scholar
  8. 8.
    L. C. Paulson. The Isabelle Reference Manual. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle98/doc/ref.dviGoogle Scholar
  9. 9.
    K. Schneider, R. Kuma, and T. Kropf. Integrating a first-order automatic prover in the HOL environment. In Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications. IEEE Computer Society Press, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Elsa L. Gunter
    • 1
  1. 1.Bell LaboratoriesMurray HillUSA

Personalised recommendations