DSpace Kolekcja:

Formalization of Quasilattices

2021-05-04T09:47:01Z

Tytuł: Formalization of Quasilattices Autorzy: Kulesza, Dominik; Grabowski, Adam Abstrakt: The main aim of this article is to introduce formally one of the generalizations of lattices, namely quasilattices, which can be obtained from the axiomatization of the former class by certain weakening of ordinary absorption laws. We show propositions QLT-1 to QLT-7 from [15], presenting also some short variants of corresponding axiom systems. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.

Grothendieck Universes

2021-05-04T09:18:14Z

Tytuł: Grothendieck Universes Autorzy: Pąk, Karol Abstrakt: The foundation of the Mizar Mathematical Library [2], is first-order Tarski-Grothendieck set theory. However, the foundation explicitly refers only to Tarski’s Axiom A, which states that for every set X there is a Tarski universe U such that X ∈ U. In this article, we prove, using the Mizar [3] formalism, that the Grothendieck name is justified. We show the relationship between Tarski and Grothendieck universe.

Multiplication-Related Classes of Complex Numbers

2021-05-04T09:02:39Z

Tytuł: Multiplication-Related Classes of Complex Numbers Autorzy: Ziobro, Rafał Abstrakt: The use of registrations is useful in shortening Mizar proofs [1], [2], both in terms of formalization time and article space. The proposed system of classes for complex numbers aims to facilitate proofs involving basic arithmetical operations and order checking. It seems likely that the use of self-explanatory adjectives could also improve legibility of these proofs, which would be an important achievement [3]. Additionally, some potentially useful definitions, following those defined for real numbers, are introduced.

Partial Correctness of a Fibonacci Algorithm

2021-05-04T08:56:31Z

Tytuł: Partial Correctness of a Fibonacci Algorithm Autorzy: Korniłowicz, Artur Abstrakt: In this paper we introduce some notions to facilitate formulating and proving properties of iterative algorithms encoded in nominative data language [19] in the Mizar system [3], [1]. It is tested on verification of the partial correctness of an algorithm computing n-th Fibonacci number: i := 0 s := 0 b := 1 c := 0 while (i <> n) c := s s := b b := c + s i := i + 1 return s This paper continues verification of algorithms [10], [13], [12] written in terms of simple-named complex-valued nominative data [6], [8], [17], [11], [14], [15]. 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 [16], [18], [7], [5].