Hilbert's Tenth Problem in Coq
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- scientific article; zbMATH DE number 3336816 (Why is no real title available?)
- A new technique for obtaining diophantine representations via elimination of bounded universal quantifiers
- Arithmetical problems and recursively enumerable predicates
- Diophantine sets. Preliminaries
- Existential Definability in Arithmetic
- Hilbert's Tenth Problem is Unsolvable
- Martin Davis and Hilbert's tenth problem
- Recursively enumerable sets of positive integers and their decision problems
- Register machine proof of the theorem on exponential diophantine representation of enumerable sets
- The Matiyasevich theorem. Preliminaries
- The decision problem for exponential diophantine equations
- 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
- Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
Cited in
(6)- scientific article; zbMATH DE number 7566048 (Why is no real title available?)
- scientific article; zbMATH DE number 7566073 (Why is no real title available?)
- Trakhtenbrot’s Theorem in Coq
- New Computational Paradigms
- 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
This page was built for publication: Hilbert's Tenth Problem in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089029)
