Towards Knowledge Management for HOL Light

DOI10.1007/978-3-319-08434-3_26zbMath1304.68158OpenAlexW42958140WikidataQ108482168 ScholiaQ108482168MaRDI QIDQ5495935

Florian Rabe, Cezary Kaliszyk

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08434-3_26

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items (6)

Classification of alignments between concepts of formal mathematical systems ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ Unnamed Item ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Experiences from exporting major proof assistant libraries ⋮ The future of logic: foundation-independence

Uses Software

• Isabelle
• Proviola
• ML
• MathWebSearch
• HOL
• HOL Light
• Nuprl
• MMT
• QMT
• OMDoc
• IMPS
• Flyspeck
• OpenTheory

Cites Work

• Unnamed Item
• A scalable module system
• IMPS: An interactive mathematical proof system
• Isabelle. A generic theorem prover
• The Mizar Mathematical Library in OMDoc: translation and applications
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Formal Mathematics on Display: A Wiki for Flyspeck
• Capturing Hiproofs in HOL Light
• The MMT API: A Generic MKM System
• Extending MKM Formats at the Statement Level
• Proviola: A Tool for Proof Re-animation
• A framework for defining logics
• A Foundational View on Integration Problems
• A Search Engine for Mathematical Formulae
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• Communicating Formal Proofs: The Case of Flyspeck
• Cooperative Repositories for Formal Proofs
• Matching Concepts across HOL Libraries
• Flexary Operators for Formalized Mathematics
• Importing HOL Light into Coq

This page was built for publication: Towards Knowledge Management for HOL Light