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

@@ Property / DOI @@
-.1007/s10817-015-9322-8
@@ Property / DOI: 10.1007/s10817-015-9322-8 / rank @@
-Normal rank
@@ Property / author @@
-Lawrence Charles Paulson
@@ Property / author: Lawrence Charles Paulson / rank @@
-Normal rank
@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B35
@@ Property / Mathematics Subject Classification ID: 03B35 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F30
@@ Property / Mathematics Subject Classification ID: 03F30 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F40
@@ Property / Mathematics Subject Classification ID: 03F40 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6585233
@@ Property / zbMATH DE Number: 6585233 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Gödel's incompleteness theorems
@@ Property / zbMATH Keywords: Gödel's incompleteness theorems / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Isabelle/HOL
@@ Property / zbMATH Keywords: Isabelle/HOL / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+nominal syntax
@@ Property / zbMATH Keywords: nominal syntax / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+formalisation of mathematics
@@ Property / zbMATH Keywords: formalisation of mathematics / rank @@
+Normal rank
@@ Property / author @@
+Lawrence Charles Paulson
@@ Property / author: Lawrence Charles Paulson / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+FinFuns
@@ Property / describes a project that uses: FinFuns / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Incompleteness Theorems
@@ Property / describes a project that uses: Incompleteness Theorems / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q56853390
@@ Property / Wikidata QID: Q56853390 / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2015224901
@@ Property / OpenAlex ID: W2015224901 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.13792
@@ Property / arXiv ID: 2104.13792 / rank @@
+Normal rank
@@ 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
@@ Property / DBLP publication ID @@
+journals/jar/Paulson15
@@ Property / DBLP publication ID: journals/jar/Paulson15 / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S10817-015-9322-8
@@ Property / DOI: 10.1007/S10817-015-9322-8 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:286772