DSpace Zespół:
http://hdl.handle.net/11320/20
2019-05-26T12:42:13ZTarski Geometry Axioms. Part IV – Right Angle
http://hdl.handle.net/11320/7842
Tytuł: Tarski Geometry Axioms. Part IV – Right Angle
Autorzy: Coghetto, Roland; Grabowski, Adam
Abstrakt: In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).2019-01-01T00:00:00ZFundamental 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].2018-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].2018-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].2018-01-01T00:00:00Z