DSpace Zespół:
http://hdl.handle.net/11320/20
Wed, 23 Jan 2019 21:29:53 GMT2019-01-23T21:29:53ZDiophantine sets. Preliminaries
http://hdl.handle.net/11320/6835
Tytuł: Diophantine sets. Preliminaries
Autorzy: Pąk, Karol
Abstrakt: In this article, we define Diophantine sets using the Mizar formalism. We focus on selected properties of multivariate polynomials, i.e., functions of several variables to show finally that the class of Diophantine sets is closed with respect to the operations of union and intersection.
This article is the next in a series [1], [5] aiming to formalize the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/68352018-01-01T00:00:00ZSequences of Prime Reciprocals. Preliminaries
http://hdl.handle.net/11320/6834
Tytuł: Sequences of Prime Reciprocals. Preliminaries
Autorzy: Grabowski, Adam
Abstrakt: In the article we formalize some properties needed to prove that sequences of prime reciprocals are divergent. The aim is to show that the series exhibits log-log growth. We introduce some auxiliary notions as harmonic numbers, telescoping series, and prove some standard properties of logarithms and exponents absent in the Mizar Mathematical Library. At the end we proceed with square-free and square-containing parts of a natural number and reciprocals of corresponding products.Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/68342018-01-01T00:00:00ZKleene Algebra of Partial Predicates
http://hdl.handle.net/11320/6830
Tytuł: Kleene Algebra of Partial Predicates
Autorzy: Korniłowicz, Artur; Ivanov, Ievgen; Nikitchenko, Mykola
Abstrakt: We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [17], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [3] (also called quasi-Boolean algebra) which satisfies the condition x ∧¬:x ⩽ y ∨¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8].
The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [3]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [16]. More details about the origin of this notion and its relation to other notions can be found in [24, 4, 1, 2]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [22, 6], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.
Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [17, 5, 18, 32, 29, 30]. A partial predicate also corresponds to the notion of a partial set [26] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, n which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [25]. In [27] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.
Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [31, 28, 33, 15], for formalizing extensions of the Floyd-Hoare logic [7, 9] which allow reasoning about properties of programs in the case of partial pre- and postconditions [23, 20, 19, 21], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [11, 13, 14, 12, 10].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/68302018-01-01T00:00:00ZTarski Geometry Axioms. Part III
http://hdl.handle.net/11320/6554
Tytuł: Tarski Geometry Axioms. Part III
Autorzy: Coghetto, Roland; Grabowski, Adam
Abstrakt: In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (“Satz”) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).Sun, 01 Jan 2017 00:00:00 GMThttp://hdl.handle.net/11320/65542017-01-01T00:00:00Z