Lemma Mining over HOL Light

DOI10.1007/978-3-642-45221-5_34zbMath1407.68437arXiv1310.2797OpenAlexW1556128154WikidataQ108482177 ScholiaQ108482177MaRDI QIDQ2870150

Cezary Kaliszyk, Josef Urban

Publication date: 17 January 2014

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Related Items

Proof mining with dependent types, JEFL: joint embedding of formal proof libraries, Learning-assisted theorem proving with millions of lemmas, HOL(y)Hammer: online ATP service for HOL Light, Matching Concepts across HOL Libraries

Uses Software

• Isabelle
• VAMPIRE
• MoMM
• Mizar
• Prover9
• HOL Light
• Mace4
• MaLeCoP
• MaSh
• E Theorem Prover
• MaLARea
• BliStr