An LCF-Style Interface between HOL and First-Order Logic

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


Performing interactive proof in the HOL theorem prover1 [3] 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 [4] 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.

Unable to display preview. Download preview PDF.


  1. 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
  2. 2.
    M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science, Springer Verlag, 1979.zbMATHGoogle Scholar
  3. 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. 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. 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. 6.
    L. C. Paulson. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 5(3), March 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Joe Hurd
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeUK

Personalised recommendations