A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772): Difference between revisions

@@ Property / cites work @@
+Q4397069
@@ Property / cites work: Q4397069 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5466245
@@ Property / cites work: Q5466245 / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+Q3244331
@@ Property / cites work: Q3244331 / rank @@
+Normal rank
@@ Property / cites work @@
+Addition and multiplication of sets
@@ Property / cites work: Addition and multiplication of sets / rank @@
+Normal rank
@@ Property / cites work @@
+Advanced logic for applications
@@ Property / cites work: Advanced logic for applications / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q3618853
@@ Property / cites work: Q3618853 / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory for verification. I: From foundations to functions
+Normal rank
@@ Property / cites work @@
+Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
+Normal rank
@@ Property / cites work @@
+Set theory. An introduction to independence proofs
+Normal rank
@@ Property / cites work @@
+Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+More Church-Rosser proofs (in Isabelle/HOL)
@@ Property / cites work: More Church-Rosser proofs (in Isabelle/HOL) / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Proof Pearl: De Bruijn Terms Really Do Work
@@ Property / cites work: Proof Pearl: De Bruijn Terms Really Do Work / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
+Normal rank
@@ Property / cites work @@
+A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
+Normal rank
@@ Property / cites work @@
+Nominal Sets
@@ Property / cites work: Nominal Sets / rank @@
+Normal rank
@@ Property / cites work @@
+Metamathematics, Machines and Gödel's Proof
@@ Property / cites work: Metamathematics, Machines and Gödel's Proof / rank @@
+Normal rank
@@ Property / cites work @@
+Finite sets and Gödel's incompleteness theorems
@@ Property / cites work: Finite sets and Gödel's incompleteness theorems / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank