The DPRM Theorem in Isabelle (Short Paper).

DOI10.4230/LIPICS.ITP.2019.33MaRDI QIDQ5875447zbMATH OpenOpenAlexFDO

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

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPIcs.ITP.2019.33

zbMATH Keywords

Diophantine predicatesDPRM theoremformal verificationHilbert's tenth problemIsabellerecursively enumerable setsregister machines

Mathematics Subject Classification ID

Cites work

• Beginners' quest to formalize mathematics: a feasibility study in Isabelle
• Formalization of the MRDP theorem in the Mizar system
• Hilbert's Tenth Problem: What was done and what is to be done
• Mechanising Turing machines and computability theory in Isabelle/HOL

Cited in

(5)

• Linear termination is undecidable
• A formal proof of complexity bounds on Diophantine equations
• GOL in GOL in HOL: verified circuits in Conway's game of life
• Lucas's Theorem
• Diophantine Equations and the DPRM Theorem

This page was built for publication: The DPRM Theorem in Isabelle (Short Paper).

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