Towards Self-verification of HOL Light
From MaRDI portal
Publication:3613408
DOI10.1007/11814771_17zbMath1222.68364OpenAlexW1606213779MaRDI QIDQ3613408
No author found.
Publication date: 12 March 2009
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814771_17
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (27)
Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm ⋮ A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ On definitions of constants and types in HOL ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Directly reflective meta-programming ⋮ Formalizing an analytic proof of the prime number theorem ⋮ Formalization of the resolution calculus for first-order logic ⋮ Proof-Producing Reflection for HOL ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Tactics for hierarchical proof ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Unnamed Item ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A verified proof checker for higher-order logic ⋮ Pollack-inconsistency ⋮ Unnamed Item ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ Formalizing Arrow's theorem ⋮ Matching Concepts across HOL Libraries ⋮ A formalization and proof checker for Isabelle's metalogic
Uses Software
This page was built for publication: Towards Self-verification of HOL Light
