Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle
Authors: Benedikt Stock, Abhik Pal, Maria Antonia Oprea, Yufei Liu, Malte Sophian Hassler, Simon Dubischar, Prabhat Devkota, Yiping Deng, Marco David, Bogdan Ciurezu, Jonas Bayer and Deepak Aryal
Paper Information
| Title: | Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle |
| Authors: | Benedikt Stock, Abhik Pal, Maria Antonia Oprea, Yufei Liu, Malte Sophian Hassler, Simon Dubischar, Prabhat Devkota, Yiping Deng, Marco David, Bogdan Ciurezu, Jonas Bayer and Deepak Aryal |
| Proceedings: | Isabelle Papers |
| Editor: | Makarius Wenzel |
| Keywords: | Hilbert's tenth problem, DPRM Theorem, Isabelle, Diophantine equations, recursively enumerable |
| Abstract: | ABSTRACT. Hilbert's tenth problem, posed in 1900 by David Hilbert, asks for a general algorithm to determine the solvability of any given Diophantine equation. In 1970, Yuri Matiyasevich proved the DPRM theorem which implies such an algorithm cannot exist. This paper will outline our attempt to formally state the DPRM theorem and verify Matiyasevich's proof using the proof assistant Isabelle/HOL. |
| Pages: | 11 |
| Talk: | Jul 13 11:30 (Session 86E: Isabelle 2) |
| Paper: |  |