Trakhtenbrot’s Theorem in Coq

DOI10.1007/978-3-030-51054-1_5OpenAlexW3046678492MaRDI QIDQ5048993

Dominique Larchey-Wendling, Dominik Kirst

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2004.07390

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Unnamed Item ⋮ Formalization of the computational theory of a Turing complete functional language model

Uses Software

• Coq
• Autosubst
• GitHub
• coq-library-undecidability

Cites Work

• On the almighty wand
• Elements of finite model theory.
• Verification of PCP-related computational reductions in Coq
• Completeness theorems for first-order logic analysed in constructive type theory
• Hereditarily Finite Sets in Constructive Type Theory
• HOCore in Coq
• Hilbert's Tenth Problem in Coq
• Pragmatic Quotient Types in Coq
• Some elementary results in intuitionistic model theory
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Trakhtenbrot’s Theorem in Coq