Dominique Larchey-Wendling

Hilbert’s Tenth Problem in Coq

Theory and Logic Group hosting a talk by Dominique Larchey-Wendling

DATE:Wednesday, November 27, 2019
TIME:16:30 s.t.
VENUE:Seminar Room Gödel, Favoritenstrasse 9-11, Ground Floor, (HB EG 10)

ABSTRACT

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.

Comments are closed.