Conversion of HOL Light proofs into Metamath

Mario M Carneiro

Abstract


We present an algorithm for converting proofs from the OpenTheory interchange format, which can be translated to and from any of the HOL family of proof languages (HOL4, HOL Light, ProofPower, and Isabelle), into the ZFC-based Metamath language. This task is divided into two steps: the translation of an OpenTheory proof into a Metamath HOL formalization, hol.mm, followed by the embedding of the HOL formalization into the main ZFC foundations of the main Metamath library, set.mm. This process provides a means to link the simplicity of the Metamath foundations to the intense automation efforts which have borne fruit in HOL Light, allowing the production of complete Metamath proofs of theorems in HOL Light, while also proving that HOL Light is consistent, relative to Metamath's ZFC axiomatization.

Keywords


metamath; opentheory; hol light; proof translation; formalization; algorithms

Full Text:

PDF (English)

References


[Far08] William M Farmer. The seven virtues of simple type theory. Journal of

Applied Logic, 6(3):267{286, 2008.

[Har09] John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias

Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of

the 22nd International Conference on Theorem Proving in Higher Order

Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science,

pages 60{66, Munich, Germany, 2009. Springer-Verlag.

[Hur11] Joe Hurd. The OpenTheory standard theory library. pages 177{191, 2011.

[Kun11] Ondrej Kuncar. Proving valid quantified boolean formulas in HOL Light.

Lecture Notes in Computer Science, 6898:184{199, 2011.

[Meg07] Norman D. Megill. Metamath: A Computer Language for Pure

Mathematics. Lulu Publishing, Morrisville, North Carolina, 2007.

http://us.metamath.org/downloads/metamath.pdf.




DOI: 10.6092/issn.1972-5787/4596

Copyright (c) 2016 Mario M Carneiro

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.