Towards Knowledge Management for HOL Light
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1863394 (Why is no real title available?)
- A Search Engine for Mathematical Formulae
- A foundational view on integration problems
- A framework for defining logics
- A machine-checked proof of the odd order theorem
- A scalable module system
- Capturing hiproofs in HOL light
- Communicating formal proofs: the case of Flyspeck
- Cooperative Repositories for Formal Proofs
- Extending MKM formats at the statement level
- Flexary operators for formalized mathematics
- Formal mathematics on display: a wiki for Flyspeck
- IMPS: An interactive mathematical proof system
- Importing HOL Light into Coq
- Isabelle. A generic theorem prover
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Matching concepts across HOL libraries
- Proviola: a tool for proof re-animation
- Scalable LCF-style proof translation
- The MMT API: a generic MKM system
- The Mizar Mathematical Library in OMDoc: translation and applications
Cited in
(7)- The future of logic: foundation-independence
- The CADE-26 automated theorem proving system competition -- CASC-26
- Towards establishing the use of holons as an enquiry method
- Classification of alignments between concepts of formal mathematical systems
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- Experiences from exporting major proof assistant libraries
- Making PVS accessible to generic services by interpretation in a universal format
Describes a project that uses
Uses Software
This page was built for publication: Towards Knowledge Management for HOL Light
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495935)
