Scalable LCF-Style Proof Translation
From MaRDI portal
Publication:5327336
DOI10.1007/978-3-642-39634-2_7zbMath1317.68214OpenAlexW11532415WikidataQ108482183 ScholiaQ108482183MaRDI QIDQ5327336
Cezary Kaliszyk, Alexander Krauss
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_7
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ JEFL: joint embedding of formal proof libraries ⋮ From informal to formal proofs in Euclidean geometry ⋮ Aligning concepts across proof assistant libraries ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ Formalising Mathematics in Simple Type Theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Experiences from exporting major proof assistant libraries ⋮ Matching Concepts across HOL Libraries ⋮ Towards Knowledge Management for HOL Light ⋮ A Vernacular for Coherent Logic ⋮ Proof Auditing Formalised Mathematics ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
