Hilbert's Tenth Problem in Coq (Extended Version)
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 prob...
Na minha lista:
| Principais autores: | , |
|---|---|
| Formato: | Artigo |
| Idioma: | Inglês |
| Publicado em: |
Logical Methods in Computer Science e.V.
2022-03-01
|
| coleção: | Logical Methods in Computer Science |
| Assuntos: | |
| Acesso em linha: | https://lmcs.episciences.org/6195/pdf |
| Tags: |
Sem tags, seja o primeiro a adicionar uma tag!
|