Conversion of HOL Light proofs into Metamath

DOI10.6092/issn.1972-5787/4596zbMath1451.68337OpenAlexW2962903681MaRDI QIDQ5195274

Mario M. Carneiro

Publication date: 18 September 2019

Full work available at URL: https://arxiv.org/abs/1412.8091

zbMATH Keywords

formalizationproof translationHol LightMetamathOpenTheory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• ProofPower
• HOL Light
• Metamath
• OpenTheory

This page was built for publication: Conversion of HOL Light proofs into Metamath