Hilbert's Tenth Problem in Coq - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Hilbert's Tenth Problem in Coq

Résumé

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem-in our case by a Minsky machine-is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer.
Fichier principal
Vignette du fichier
LIPIcs-FSCD-2019-27.pdf (607.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02333404 , version 1 (25-10-2019)

Identifiants

Citer

Dominique Larchey-Wendling, Yannick Forster. Hilbert's Tenth Problem in Coq. 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Jun 2019, Dortmund, Germany. pp.27:1--27:20, ⟨10.4230/LIPIcs.FSCD.2019.27⟩. ⟨hal-02333404⟩
211 Consultations
223 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More