Zobrazeno 1 - 10
of 61
pro vyhledávání: '"Karol Pąk"'
Autor:
Dominik Tomaszuk, Karol Pąk
Publikováno v:
PLoS ONE, Vol 13, Iss 2, p e0191917 (2018)
Graph databases are constantly growing, and, at the same time, some of their data is the same or similar. Our experience with the management of the existing databases, especially the bigger ones, shows that certain vertices are particularly replicate
Externí odkaz:
https://doaj.org/article/d75d31076422424d8302479aa5634164
Autor:
Karol Pąk
Publikováno v:
Logical Methods in Computer Science, Vol Volume 10, Issue 3 (2014)
In formal proof checking environments such as Mizar it is not merely the validity of mathematical formulas that is evaluated in the process of adoption to the body of accepted formalizations, but also the readability of the proofs that witness validi
Externí odkaz:
https://doaj.org/article/389bbcd04c3645a18736a4641a5dd835
Autor:
Karol Pąk
Publikováno v:
Formalized Mathematics. 30:255-279
Summary In this article we formalize in Mizar [1], [2] the final step of our attempt to formally construct a prime representing polynomial with 10 variables proposed by Yuri Matiyasevich in [4]. The first part of the article includes many auxiliary l
Autor:
Cezary Kaliszyk, Karol Pąk
Publikováno v:
Journal of Automated Reasoning. 67
The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic
Autor:
Karol Pąk
Publikováno v:
Formalized Mathematics. 29:221-228
Summary The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this problem, using the Mizar system [1], [2], in two independent ways, proving the exist
Autor:
Karol Pąk
Publikováno v:
Formalized Mathematics, Vol 28, Iss 2, Pp 211-215 (2020)
Summary The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such tha
Autor:
Karol Pąk
Publikováno v:
Formalized Mathematics, Vol 27, Iss 2, Pp 197-208 (2019)
Summary The 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
Autor:
Karol Pąk
Publikováno v:
Formalized Mathematics, Vol 27, Iss 2, Pp 209-221 (2019)
Summary 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 solv
Autor:
Chad E. Brown, Karol Pąk
Publikováno v:
Formalized Mathematics
Formalized Mathematics, Vol 27, Iss 4, Pp 321-335 (2019)
Formalized Mathematics, Vol 27, Iss 4, Pp 321-335 (2019)
Summary In this article, we prove, using the Mizar [2] formalism, a number of properties that correspond to the AIM Conjecture. In the first section, we define division operations on loops, inner mappings T, L and R, commutators and associators and b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::001a549185455bb4a5676edf603cfe97
https://zenodo.org/record/4570819
https://zenodo.org/record/4570819
Autor:
Karol Pąk, Marcin Acewicz
Publikováno v:
Formalized Mathematics, Vol 26, Iss 2, Pp 175-181 (2018)
Summary 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 show