REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2019, Volume 27, Issue 2

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/8127
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorPąk, Karol-
    dc.date.accessioned2019-07-29T08:28:46Z-
    dc.date.available2019-07-29T08:28:46Z-
    dc.date.issued2019-
    dc.identifier.citationFormalized Mathematics, Volume 27, Issue 2, Pages 197 - 208-
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/8127-
    dc.description.abstractThe article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant [3], [6], [4]. We analyze four equations from the Diophantine standpoint that are crucial in the bounded quantifier theorem, that is used in one of the approaches to solve the problem.Based on our previous work [1], we prove that the value of a given binomial coefficient and factorial can be determined by its arguments in a Diophantine way. Then we prove that two productsz=∏i=1x(1+i⋅y),        z=∏i=1x(y+1-j),      (0.1)where y > x are Diophantine.The formalization follows [10], Z. Adamowicz, P. Zbierski [2] as well as M. Davis [5].-
    dc.language.isoen-
    dc.publisherDeGruyter Open-
    dc.subjectHilbert’s 10th problem-
    dc.subjectDiophantine relations-
    dc.subject11D45-
    dc.subject68T99-
    dc.subject03B35-
    dc.titleDiophantine Sets. Part II-
    dc.typeArticle-
    dc.identifier.doi10.2478/forma-2019-0019-
    dc.description.AffiliationInstitute of Informatics, University of Białystok, Poland-
    dc.description.referencesMarcin Acewicz and Karol Pąk. Basic Diophantine relations. Formalized Mathematics, 26(2):175–181, 2018. doi:10.2478/forma-2018-0015.-
    dc.description.referencesZofia 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.referencesGrzegorz 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.referencesGrzegorz 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.referencesMartin 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.referencesAdam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.-
    dc.description.referencesArtur Korniłowicz and Karol Pąk. Basel problem – preliminaries. Formalized Mathematics, 25(2):141–147, 2017. doi:10.1515/forma-2017-0013.-
    dc.description.referencesXiquan Liang, Li Yan, and Junjie Zhao. Linear congruence relation and complete residue systems. Formalized Mathematics, 15(4):181–187, 2007. doi:10.2478/v10037-007-0022-7.-
    dc.description.referencesKarol Pąk. Diophantine sets. Preliminaries. Formalized Mathematics, 26(1):81–90, 2018. doi:10.2478/forma-2018-0007.-
    dc.description.referencesCraig Alan Smorynski. Logical Number Theory I, An Introduction. Universitext. Springer-Verlag Berlin Heidelberg, 1991. ISBN 978-3-642-75462-3.-
    dc.description.referencesTetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.-
    dc.description.referencesRafał Ziobro. On subnomials. Formalized Mathematics, 24(4):261–273, 2016. doi:10.1515/forma-2016-0022.-
    dc.identifier.eissn1898-9934-
    dc.description.volume27-
    dc.description.issue2-
    dc.description.firstpage197-
    dc.description.lastpage208-
    dc.identifier.citation2Formalized Mathematics-
    dc.identifier.orcid0000-0002-7099-1669-
    Występuje w kolekcji(ach):Artykuły naukowe (WInf)
    Formalized Mathematics, 2019, Volume 27, Issue 2

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    forma_2019_27_2_010.pdf274,91 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


    Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons