Hilbert's Tenth Problem in Coq

DOI10.4230/LIPIcs.FSCD.2019.27OpenAlexW2953924437MaRDI QIDQ5089029

Dominique Larchey-Wendling, Yannick Forster

Publication date: 18 July 2022

Full work available at URL: https://hal.archives-ouvertes.fr/hal-02333404

zbMATH Keywords

undecidabilityreductioncomputability theorytype theoryDiophantine equationsMinsky machinesCoqHilbert's tenth problemFRACTRAN

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Related Items (5)

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

Cites Work

• Unnamed Item
• Unnamed Item
• The decision problem for exponential diophantine equations
• The undecidability of the second-order unification problem
• Weak call-by-value lambda calculus as a model of computation in Coq
• Typing total recursive functions in Coq
• Verification of PCP-related computational reductions in Coq
• The Matiyasevich theorem. Preliminaries
• Diophantine sets. Preliminaries
• A new technique for obtaining diophantine representations via elimination of bounded universal quantifiers
• Martin Davis and Hilbert’s Tenth Problem
• Register machine proof of the theorem on exponential diophantine representation of enumerable sets
• Hilbert's Tenth Problem is Unsolvable
• Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
• Existential Definability in Arithmetic
• Arithmetical problems and recursively enumerable predicates
• Recursively enumerable sets of positive integers and their decision problems

This page was built for publication: Hilbert's Tenth Problem in Coq