A formally verified abstract account of Gödel's incompleteness theorems
From MaRDI portal
Publication:2305432
DOI10.1007/978-3-030-29436-6_26OpenAlexW2969786701MaRDI QIDQ2305432
Andrei Popescu, Dmitriy Traytel
Publication date: 10 March 2020
Full work available at URL: https://eprints.mdx.ac.uk/28147/1/Goedel_CADE_2019.pdf
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version, Formalizing Bachmair and Ganzinger's ordered resolution prover, Distilling the requirements of Gödel's incompleteness theorems with a proof assistant, A formally verified abstract account of Gödel's incompleteness theorems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
- Abstract proof checking: An example motivated by an incompleteness theorem
- Automated search for Gödel's proofs
- Mathematical logic. On numbers, sets, structures, and symmetry
- HOL(y)Hammer: online ATP service for HOL Light
- The scope of Gödel's first incompleteness theorem
- A formally verified abstract account of Gödel's incompleteness theorems
- Term-generic logic
- Institution-independent model theory
- Undecidable theories
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
- A Consistent Foundation for Isabelle/HOL
- Comprehending Isabelle/HOL’s Consistency
- Unified Classical Logic Completeness
- Solution of a problem of Leon Henkin
- Nominal (Universal) Algebra: Equational Logic with Names and Binding
- Metamathematics, Machines and Gödel's Proof
- Institutions: abstract model theory for specification and programming
- Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem
- GENERALIZATIONS OF GÖDEL’S INCOMPLETENESS THEOREMS FOR ∑n-DEFINABLE THEORIES OF ARITHMETIC
- Finite sets and Gödel's incompleteness theorems
- Theorem Proving in Higher Order Logics
- An automatic proof of Gödel's incompleteness theorem
- Formalizing Bachmair and Ganzinger's ordered resolution prover
