scientific article; zbMATH DE number 7566048

MaRDI QIDQ5094119zbMATH OpenFDO

Authors Dominique Larchey-Wendling, Yannick Forster

Publication date 2 August 2022

Full work available at URL https://arxiv.org/abs/2003.04604, https://lmcs.episciences.org/9153

zbMATH Keywords

computability theoryCoqDiophantine equationsFractranHilbert's tenth problemMinsky machinesreductiontype theoryundecidability

Mathematics Subject Classification ID

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

Recommendations

• Hilbert's Tenth Problem in Coq
• Hilbert's tenth problem for weak theories of arithmetic
• Extensions of Hilbert's tenth problem
• Extensions of Hilbert's tenth problem: definability and decidability in number theory
• New Computational Paradigms
• Hilbert's tenth problem. An introduction to logic, number theory, and computability
• Bar-Hillel theorem mechanization in Coq
• Theorem Proving in Higher Order Logics
• Hilbert's Tenth Problem: What was done and what is to be done
• Proof by computation in the Coq system

Cites work

• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• A new technique for obtaining diophantine representations via elimination of bounded universal quantifiers
• A simpler undecidability proof for system F inhabitation
• Arithmetical problems and recursively enumerable predicates
• Categoricity results for second-order ZF in dependent type theory
• Diophantine sets. Preliminaries
• Existential Definability in Arithmetic
• Hilbert's Tenth Problem in Coq
• Hilbert's Tenth Problem is Unsolvable
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• scientific article; zbMATH DE number 7699436 (Why is no real title available?)
• Martin Davis and Hilbert's tenth problem
• Mechanising Turing machines and computability theory in Isabelle/HOL
• Recursively enumerable sets of positive integers and their decision problems
• Register machine proof of the theorem on exponential diophantine representation of enumerable sets
• The decision problem for exponential diophantine equations
• The Matiyasevich theorem. Preliminaries
• The undecidability of the second-order unification problem
• Typing total recursive functions in Coq
• Verification of PCP-related computational reductions in Coq
• Weak call-by-value lambda calculus as a model of computation in Coq

Cited in

(2)

• Hilbert's Tenth Problem in Coq
• Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)

Describes a project that uses

Uses Software

• Coq
• FRACTRAN

This page was built for publication:

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