swMATH17594MaRDI QIDQ29451FDOQ29451
Author name not available (Why is that?)
Official website: http://www.proof-technologies.com/holzero/
Cited In (19)
- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- On definitions of constants and types in HOL
- A formal proof of the Kepler conjecture
- A verified proof checker for higher-order logic
- ProofPower
- HOL-Omega
- Milawa
- Jitawa
- HOL Zero's solutions for Pollack-inconsistency
- HOL90
- Light-weight Containers
- Metamath Zero
- A formalization and proof checker for Isabelle's metalogic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Flyspecking Flyspeck
- Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
- A consistent foundation for Isabelle/HOL
This page was built for software: HOL Zero
