Sharing HOL4 and HOL Light Proof Knowledge

DOI10.1007/978-3-662-48899-7_26zbMath1471.68309arXiv1509.03527WikidataQ108482162 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

Mathematics Subject Classification ID

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

68V30: Mathematical knowledge management

Uses Software

• Isabelle/HOL
• HOL
• HOL Light
• HOLyHammer