Trakhtenbrot’s Theorem in Coq

DOI10.1007/978-3-030-51054-1_5MaRDI QIDQ5048993zbMATH OpenOpenAlexFDO

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

• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• scientific article; zbMATH DE number 3057871 (Why is no real title available?)
• An efficient Coq tactic for deciding Kleene algebras
• Completeness theorems for first-order logic analysed in constructive type theory
• Elements of finite model theory.
• HOCore in Coq
• Hereditarily finite sets in constructive type theory
• Hilbert's Tenth Problem in Coq
• On the almighty wand
• Pragmatic quotient types in Coq
• Some elementary results in intuitionistic model theory
• Verification of PCP-related computational reductions in Coq

Cited in

(5)

• Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
• Formalization of the computational theory of a Turing complete functional language model
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
• An analysis of Tennenbaum's theorem in constructive type theory

Describes a project that uses

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)