Towards Knowledge Management for HOL Light
From MaRDI portal
Publication:5495935
DOI10.1007/978-3-319-08434-3_26zbMath1304.68158OpenAlexW42958140WikidataQ108482168 ScholiaQ108482168MaRDI QIDQ5495935
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
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
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