scientific article; zbMATH DE number 7566048

MaRDI QIDQ5094119

Yannick Forster, Dominique Larchey-Wendling

Publication date: 2 August 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

undecidabilityreductioncomputability theorytype theoryDiophantine equationsMinsky machinesCoqHilbert's tenth problemFractran

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)

Uses Software

• Coq
• FRACTRAN

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• Categoricity results for second-order ZF in dependent type theory
• 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
• Hilbert's Tenth Problem in Coq
• Mechanising Turing Machines and Computability Theory in Isabelle/HOL
• Existential Definability in Arithmetic
• Arithmetical problems and recursively enumerable predicates
• 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]