Adding external decision procedures to HOL90 securely
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.
KeywordsModel Check Inference Rule Decision Procedure Free Variable Computer Algebra System
Unable to display preview. Download preview PDF.
- 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.M. J. C. Gordon and T. Melham, Introduction to HOL. Cambridge University Press, 1993.Google Scholar
- 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
- 5.G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall Software Series, 1991.Google Scholar
- 6.K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.Google Scholar
- 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.L. C. Paulson. The Isabelle Reference Manual. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle98/doc/ref.dviGoogle Scholar
- 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