DSpace Zesp&#243;&#322;: http://hdl.handle.net/11320/20 2019-08-22T04:10:15Z 2019-08-22T04:10:15Z Partial Correctness of a Factorial Algorithm Jaszczak, Adrian Korniłowicz, Artur http://hdl.handle.net/11320/8135 2019-07-30T07:52:23Z 2019-01-01T00:00:00Z Tytu&#322;: Partial Correctness of a Factorial Algorithm Autorzy: Jaszczak, Adrian; Korniłowicz, Artur Abstrakt: In this paper we present a formalization in the Mizar system , of the partial correctness of the algorithm: i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data ).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data ,,,,,. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data . Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic , with partial pre- and post-conditions ,,,. 2019-01-01T00:00:00Z Partial Correctness of a Power Algorithm Jaszczak, Adrian http://hdl.handle.net/11320/8136 2019-07-30T07:54:57Z 2019-01-01T00:00:00Z Tytu&#322;: Partial Correctness of a Power Algorithm Autorzy: Jaszczak, Adrian Abstrakt: This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data ,,,,,. In this paper we present a formalization in the Mizar system , of the partial correctness of the algorithm: i := val.1 j := val.2 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data ).The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data . Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic , with partial pre- and post-conditions ,,,. 2019-01-01T00:00:00Z Formalization of the MRDP Theorem in the Mizar System Pąk, Karol http://hdl.handle.net/11320/8128 2019-07-30T07:58:12Z 2019-01-01T00:00:00Z Tytu&#322;: Formalization of the MRDP Theorem in the Mizar System Autorzy: Pąk, Karol 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 . 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  and its solutions considered as two sequences {xi(a)}i=0∞,{yi(a)}i=0∞. We showed in  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 .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 , ,  follows , Z. Adamowicz, P. Zbierski  as well as M. Davis . 2019-01-01T00:00:00Z Diophantine Sets. Part II Pąk, Karol http://hdl.handle.net/11320/8127 2019-07-30T07:56:20Z 2019-01-01T00:00:00Z Tytu&#322;: Diophantine Sets. Part II Autorzy: Pąk, Karol Abstrakt: The article is the next in a series aiming to formalize the MDPR-theorem using the Mizar proof assistant , , . 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 , 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 , Z. Adamowicz, P. Zbierski  as well as M. Davis . 2019-01-01T00:00:00Z