Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)



Dear All,

Larchey-Wendling and Forster recently finished a complete formalization of the Davis-Putnam-Robinson-Matiyasevich theorem (Hilbert’s 10th problem) in Coq.  The paper is under review, the pdf is at http://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf.  The theorems in the paper are linked to the Coq development so that the Coq code can be looked at online.  The worked described in the paper contributes 12k loc to a Coq library of undecidable problems, see https://github.com/uds-psl/coq-library-undecidability.

Gert Smolka






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.