License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.33
URN: urn:nbn:de:0030-drops-110883
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11088/
Go to the corresponding LIPIcs Volume Portal

Bayer, Jonas ; David, Marco ; Pal, Abhik ; Stock, Benedikt ; Schleicher, Dierk

The DPRM Theorem in Isabelle (Short Paper)

pdf-format:
LIPIcs-ITP-2019-33.pdf (0.4 MB)

Abstract

Hilbert's 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich's proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations.

BibTeX - Entry

@InProceedings{bayer_et_al:LIPIcs:2019:11088,
  author =	{Jonas Bayer and Marco David and Abhik Pal and Benedikt Stock and Dierk Schleicher},
  title =	{{The DPRM Theorem in Isabelle (Short Paper)}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{33:1--33:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11088},
  URN =		{urn:nbn:de:0030-drops-110883},
  doi =		{10.4230/LIPIcs.ITP.2019.33},
  annote =	{Keywords: DPRM theorem, Hilbert's tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification}
}

Keywords: DPRM theorem, Hilbert's tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: Isabelle formalisation: https://gitlab.com/hilbert-10/dprm

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI