DSpace Zespół:
http://hdl.handle.net/11320/20
Mon, 20 May 2019 22:10:57 GMT2019-05-20T22:10:57ZFundamental Properties of Fuzzy Implications
http://hdl.handle.net/11320/7638
Tytuł: Fundamental Properties of Fuzzy Implications
Autorzy: Grabowski, Adam
Abstrakt: In the article we continue in the Mizar system [8], [2] the formalization of fuzzy implications according to the monograph of Baczyński and Jayaram “Fuzzy Implications” [1]. We develop a framework of Mizar attributes allowing us for a smooth proving of basic properties of these fuzzy connectives [9]. We also give a set of theorems about the ordering of nine fundamental implications: Łukasiewicz (ILK), Gödel (IGD), Reichenbach (IRC), Kleene-Dienes (IKD), Goguen (IGG), Rescher (IRS), Yager (IYG), Weber (IWB), and Fodor (IFD).This work is a continuation of the development of fuzzy sets in Mizar [6]; it could be used to give a variety of more general operations on fuzzy sets [13]. The formalization follows [10], [5], and [4].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/76382018-01-01T00:00:00ZFormalizing Two Generalized Approximation Operators
http://hdl.handle.net/11320/7628
Tytuł: Formalizing Two Generalized Approximation Operators
Autorzy: Grabowski, Adam; Sielwiesiuk, Michał
Abstrakt: Rough sets, developed by Pawlak [15], are important tool to describe situation of incomplete or partially unknown information. In this article we give the formal characterization of two closely related rough approximations, along the lines proposed in a paper by Gomolińska [2]. We continue the formalization of rough sets in Mizar [1] started in [6].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/76282018-01-01T00:00:00ZBasic Diophantine Relations
http://hdl.handle.net/11320/7627
Tytuł: Basic Diophantine Relations
Autorzy: Acewicz, Marcin; Pąk, Karol
Abstrakt: 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].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/76272018-01-01T00:00:00ZPartial Correctness of GCD Algorithm
http://hdl.handle.net/11320/7626
Tytuł: Partial Correctness of GCD Algorithm
Autorzy: Ivanov, Ievgen; Korniłowicz, Artur; Nikitchenko, Mykola
Abstrakt: In this paper we present a formalization in the Mizar system [2, 1] of the correctness of the subtraction-based version of Euclid’s algorithm computing the greatest common divisor of natural numbers. The algorithm is written in terms of simple-named complex-valued nominative data [11, 4].The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [7]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions [8, 10, 5, 3].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/76262018-01-01T00:00:00Z