Trakhtenbrot’s Theorem in Coq

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

Authors: Dominik Kirst, Dominique Larchey-Wendling 

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)

Cites Work

• Elements of finite model theory.
• Title not available (Why is that?)
• Title not available (Why is that?)
• An efficient Coq tactic for deciding Kleene algebras
• On the almighty wand
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some elementary results in intuitionistic model theory
• Title not available (Why is that?)
• Pragmatic quotient types in Coq
• Hereditarily finite sets in constructive type theory
• Verification of PCP-related computational reductions in Coq
• HOCore in Coq
• Hilbert's Tenth Problem in Coq
• Completeness theorems for first-order logic analysed in constructive type theory

Cited In (4)

• Title not available (Why is that?)
• An analysis of Tennenbaum's theorem in constructive type theory
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
• Formalization of the computational theory of a Turing complete functional language model

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5048993)