DSpace Zespół:http://hdl.handle.net/11320/202019-10-23T01:45:37Z2019-10-23T01:45:37ZPartial Correctness of a Factorial AlgorithmJaszczak, AdrianKorniłowicz, Arturhttp://hdl.handle.net/11320/81352019-07-30T07:52:23Z2019-01-01T00:00:00ZTytuł: Partial Correctness of a Factorial Algorithm
Autorzy: Jaszczak, Adrian; Korniłowicz, Artur
Abstrakt: In this paper we present a formalization in the Mizar system [3],[1] 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 [16]).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].2019-01-01T00:00:00ZPartial Correctness of a Power AlgorithmJaszczak, Adrianhttp://hdl.handle.net/11320/81362019-07-30T07:54:57Z2019-01-01T00:00:00ZTytuł: 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 [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] 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 [17]).The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [14],[16],[7],[5].2019-01-01T00:00:00ZFormalization of the MRDP Theorem in the Mizar SystemPąk, Karolhttp://hdl.handle.net/11320/81282019-07-30T07:58:12Z2019-01-01T00:00:00ZTytuł: 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 [2]. 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 [8] and its solutions considered as two sequences {xi(a)}i=0∞,{yi(a)}i=0∞. We showed in [1] 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 [9].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 [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].2019-01-01T00:00:00ZDiophantine Sets. Part IIPąk, Karolhttp://hdl.handle.net/11320/81272019-07-30T07:56:20Z2019-01-01T00:00:00ZTytuł: 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 [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].2019-01-01T00:00:00Z