REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/8128`
 Tytuł: Formalization of the MRDP Theorem in the Mizar System Autorzy: Pąk, Karol Słowa kluczowe: Hilbert’s 10th problemDiophantine relations11D4568T9903B35 Data wydania: 2019 Data dodania: 29-lip-2019 Wydawca: DeGruyter Open Źródło: Formalized Mathematics, Volume 27, Issue 2, Pages 209 - 221 Abstrakt: This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form x2 − (a2 − 1)y2 = 1 [8] and its solutions considered as two sequences {xi(a)}i=0∞,{yi(a)}i=0∞. We showed in [1] that the n-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation x = yi(a) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function y = xz is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9].In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that every recursively enumerable set is Diophantine, where recursively enumerable sets have been defined by the Martin Davis normal form.The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6]. Afiliacja: Institute of Informatics, University of Białystok, Poland URI: http://hdl.handle.net/11320/8128 DOI: 10.2478/forma-2019-0020 ISSN: 1426-2630 e-ISSN: 1898-9934 metadata.dc.identifier.orcid: 0000-0002-7099-1669 Typ Dokumentu: Article Występuje w kolekcji(ach): Artykuły naukowe (WInf)Formalized Mathematics, 2019, Volume 27, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat