Pages that link to "Item:Q3613408"
From MaRDI portal
The following pages link to Towards Self-verification of HOL Light (Q3613408):
Displaying 29 items.
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Tactics for hierarchical proof (Q626933) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- Formalizing Arrow's theorem (Q1040010) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (Q2360828) (← links)
- Formalizing an analytic proof of the prime number theorem (Q2655322) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- (Q3024890) (← links)
- Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
- A Verified Runtime for a Verified Theorem Prover (Q3088011) (← links)
- (Q5091146) (← links)
- Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
- Pollack-inconsistency (Q5170237) (← links)
- A FORMAL PROOF OF THE KEPLER CONJECTURE (Q5280247) (← links)
- Steps towards Verified Implementations of HOL Light (Q5327372) (← links)
- Matching Concepts across HOL Libraries (Q5495929) (← links)
- (Q6060676) (← links)
