An LCF-Style Interface between HOL and First-Order Logic
- 302 Downloads
Performing interactive proof in the HOL theorem prover1  involves reducing goals to simpler subgoals. It turns out that many of these subgoals can be efficiently ‘finished off’ by an automatic first-order prover. To fill this niche, Harrison implemented a version of the MESON procedure  with the ability to translate proofs to higher-order logic. This was integrated as a HOL tactic in 1996, and has since become a standard workhorse of interactive proof. Today, building all the theories in the most recent distribution of HOL relies on MESON to prove 1726 subgoals.
Unable to display preview. Download preview PDF.
- 1.Marc Bezem, Dimitri Hendriks, and Hans de Nivelle. Automated proof construction in type theory using resolution. In David A. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of Lecture Notes in Computer Science, pages 148–163, Pittsburgh, PA, USA, June 2000. Springer.Google Scholar
- 3.M. J. C. Gordon and T. F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993.Google Scholar
- 4.John Harrison. Optimizing proof search in model elimination. In Michael A. McRobbie and John K. Slaney, editors, 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, pages 313–327, New Brunswick, NJ, USA, July 1996. Springer.Google Scholar
- 5.R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL’ 91), August 1991, pages 170–176, Davis, CA, USA, 1992. IEEE Computer Society Press.Google Scholar
- 6.L. C. Paulson. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 5(3), March 1999.Google Scholar