Conversion of HOL Light proofs into Metamath

Conversion of HOL Light proofs into Metamath

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 o...

Full description

Bibliographic Details
Main Author: Mario M Carneiro
Format: Article
Language:English
Published: University of Bologna 2016-01-01
Series:Journal of Formalized Reasoning
Subjects:
metamath
opentheory
hol light
proof translation
formalization
algorithms
Online Access:http://jfr.unibo.it/article/view/4596

Internet

http://jfr.unibo.it/article/view/4596

Similar Items