arXiv:1412.8091cs.LO
Conversion of HOL Light proofs into Metamath
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, $\mathtt{\text{hol.mm}}$, followed by the embedding of the HOL formalization into the main ZFC foundations of the main Metamath library, $\mathtt{\text{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.
There has been some work to translate between systems. For example, see "Conversion of HOL Light proofs into Metamath" by Mario Carneiro, 2014: https://arxiv.org/abs/1412.8091 However, it turns out to be non-trivial, so it is not typically done in practice. Formalization…
dwheelerView on HNParent context
Different systems can have very different logical foundations, so converting proofs from a system to another can be very complicated in general. Even when converting is possible, the converted proof might be very anti-idiomatic in the target system, in more or less the same way…
giomasceView on HNParent context