Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/7627
Tytuł: | Basic Diophantine Relations |
Autorzy: | Acewicz, Marcin Pąk, Karol |
Słowa kluczowe: | Hilbert’s 10th problem Diophantine relations |
Data wydania: | 2018 |
Data dodania: | 4-mar-2019 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 26, Issue 2, Pages 175-181 |
Abstrakt: | The main purpose of formalization is to prove that two equations ya(z)= y, y = xz are Diophantine. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.In our previous work [6], we showed that from the diophantine standpoint these equations can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities. In this formalization, we express these relations in terms of Diophantine set introduced in [7]. We prove that these relations are Diophantine and then we prove several second-order theorems that provide the ability to combine Diophantine relation using conjunctions and alternatives as well as to substitute the right-hand side of a given Diophantine equality as an argument in a given Diophantine relation. Finally, we investigate the possibilities of our approach to prove that the two equations, being the main purpose of this formalization, are Diophantine.The formalization by means of Mizar system [3], [2] follows Z. Adamowicz, P. Zbierski [1] as well as M. Davis [4]. |
Afiliacja: | Marcin Acewicz - Institute of Informatics, University of Białystok, Poland Karol Pąk - Institute of Informatics, University of Białystok, Poland |
Sponsorzy: | This work has been financed by the resources of the Polish National Science Centre granted by decision no. DEC-2015/19/D/ST6/01473. |
URI: | http://hdl.handle.net/11320/7627 |
DOI: | 10.2478/forma-2018-0015 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | brakorcid 0000-0002-7099-1669 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Artykuły naukowe (WInf) Formalized Mathematics, 2018, Volume 26, Issue 2 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2018_26_2_008.pdf | 238,9 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL