Sharing HOL4 and HOL Light Proof Knowledge
From MaRDI portal
Publication:3460068
DOI10.1007/978-3-662-48899-7_26zbMath1471.68309arXiv1509.03527OpenAlexW2229278275WikidataQ108482162 ScholiaQ108482162MaRDI QIDQ3460068
Cezary Kaliszyk, Thibault Gauthier
Publication date: 12 January 2016
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1509.03527
Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Mathematical knowledge management (68V30)
Related Items (6)
Classification of alignments between concepts of formal mathematical systems ⋮ JEFL: joint embedding of formal proof libraries ⋮ ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description) ⋮ Aligning concepts across proof assistant libraries ⋮ Combining higher-order logic with set theory formalizations ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
Uses Software
This page was built for publication: Sharing HOL4 and HOL Light Proof Knowledge
