Pages that link to "Item:Q286772"

The following pages link to A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772):

Displaying 18 items.

• Theory of symbolic expressions. II (Q1075757) (← links)
• Automated proofs of Löb's theorem and Gödel's two incompleteness theorems (Q1110495) (← links)
• Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
• Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
• A formally verified abstract account of Gödel's incompleteness theorems (Q2305432) (← links)
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
• Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
• Hereditarily Finite Sets in Constructive Type Theory (Q2829273) (← links)
• A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS (Q2940885) (← links)
• A Formalisation of Finite Automata Using Hereditarily Finite Sets (Q3454094) (← links)
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF (Q3507465) (← links)
• Programming and verifying a declarative first-order prover in Isabelle/HOL (Q5145439) (← links)
• Generic Authenticated Data Structures, Formally. (Q5875417) (← links)
• Undecidable problems in quantum field theory (Q6049665) (← links)
• (Q6060676) (← links)
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting (Q6108811) (← links)
• A step towards absolute versions of metamathematical results (Q6150669) (← links)
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version (Q6156642) (← links)