Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
From MaRDI portal
Publication:6156642
DOI10.1007/s10817-022-09647-xMaRDI QIDQ6156642
Publication date: 14 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
undecidabilityfirst-order logicconstructive type theoryPeano arithmeticincompletenessCoqZF set theorysynthetic computability
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
- Finitary set theory
- Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
- Abstract proof checking: An example motivated by an incompleteness theorem
- Verification of PCP-related computational reductions in Coq
- The \textsc{MetaCoq} project
- A formally verified abstract account of Gödel's incompleteness theorems
- Hereditarily Finite Sets in Constructive Type Theory
- HOCore in Coq
- Church's thesis without tears
- Automated Search for Gödel’s Proofs
- Alfred Tarski and decidable theories
- On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation
- Completeness theorems for first-order logic analysed in constructive type theory
- Trakhtenbrot’s Theorem in Coq
- Hilbert's Tenth Problem in Coq
- Theorem Proving in Higher Order Logics
- An Efficient Coq Tactic for Deciding Kleene Algebras
- A note on the Entscheidungsproblem
- Recursively enumerable sets of positive integers and their decision problems
- [https://portal.mardi4nfdi.de/wiki/Publication:5875425 A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus]
This page was built for publication: Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
