Conversion of HOL Light proofs into Metamath

Authors

  • Mario M Carneiro Department of Mathematics, Ohio State University, Columbus OH 43210, USA

DOI:

https://doi.org/10.6092/issn.1972-5787/4596

Keywords:

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

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.

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.

Downloads

Published

2016-01-29

How to Cite

Carneiro, M. M. (2016). Conversion of HOL Light proofs into Metamath. Journal of Formalized Reasoning, 9(1), 187–200. https://doi.org/10.6092/issn.1972-5787/4596

Issue

Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto

Section

QED 20th anniversary

License

Copyright (c) 2016 Mario M Carneiro

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy