Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/7627
Pełny rekord metadanych
Pole DC | Wartość | Język |
---|---|---|
dc.contributor.author | Acewicz, Marcin | - |
dc.contributor.author | Pąk, Karol | - |
dc.date.accessioned | 2019-03-04T10:26:09Z | - |
dc.date.available | 2019-03-04T10:26:09Z | - |
dc.date.issued | 2018/07/01 | - |
dc.identifier.citation | Formalized Mathematics, Volume 26, Issue 2, Pages 175-181 | - |
dc.identifier.issn | 1426-2630 | - |
dc.identifier.uri | http://hdl.handle.net/11320/7627 | - |
dc.description.abstract | 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]. | - |
dc.description.sponsorship | This work has been financed by the resources of the Polish National Science Centre granted by decision no. DEC-2015/19/D/ST6/01473. | - |
dc.language.iso | en | - |
dc.publisher | DeGruyter Open | - |
dc.subject | Hilbert’s 10th problem | - |
dc.subject | Diophantine relations | - |
dc.title | Basic Diophantine Relations | - |
dc.type | Article | - |
dc.identifier.doi | 10.2478/forma-2018-0015 | - |
dc.description.Affiliation | Marcin Acewicz - Institute of Informatics, University of Białystok, Poland | - |
dc.description.Affiliation | Karol Pąk - Institute of Informatics, University of Białystok, Poland | - |
dc.description.references | Zofia Adamowicz and Paweł Zbierski. Logic of Mathematics: A Modern Course of Classical Logic. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley-Interscience, 1997. | - |
dc.description.references | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17. | - |
dc.description.references | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6. | - |
dc.description.references | Martin Davis. Hilbert’s tenth problem is unsolvable. The American Mathematical Monthly, Mathematical Association of America, 80(3):233–269, 1973. doi:10.2307/2318447. | - |
dc.description.references | Yatsuka Nakamura and Hisashi Ito. Basic properties and concept of selected subsequence of zero based finite sequences. Formalized Mathematics, 16(3):283–288, 2008. doi:10.2478/v10037-008-0034-y. | - |
dc.description.references | Karol Pąk. The Matiyasevich theorem. Preliminaries. Formalized Mathematics, 25(4): 315–322, 2017. doi:10.1515/forma-2017-0029. | - |
dc.description.references | Karol Pąk. Diophantine sets. Preliminaries. Formalized Mathematics, 26(1):81–90, 2018. doi:10.2478/forma-2018-0007. | - |
dc.description.references | Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001. | - |
dc.identifier.eissn | 1898-9934 | - |
dc.description.volume | 26 | - |
dc.description.issue | 2 | - |
dc.description.firstpage | 175 | - |
dc.description.lastpage | 181 | - |
dc.identifier.citation2 | Formalized Mathematics | - |
dc.identifier.orcid | brakorcid | - |
dc.identifier.orcid | 0000-0002-7099-1669 | - |
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