DSpace Kolekcja:http://hdl.handle.net/11320/55502020-11-28T16:19:18Z2020-11-28T16:19:18ZEmbedded Lattice and Properties of Gram MatrixFuta, YuichiShidama, Yasunarihttp://hdl.handle.net/11320/55712017-10-05T23:14:34Z2017-01-01T00:00:00ZTytuł: Embedded Lattice and Properties of Gram Matrix
Autorzy: Futa, Yuichi; Shidama, Yasunari
Abstrakt: In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [16] and cryptographic systems with lattice [17].2017-01-01T00:00:00ZOrdered Rings and FieldsSchwarzweller, Christophhttp://hdl.handle.net/11320/55702017-10-05T23:14:33Z2017-01-01T00:00:00ZTytuł: Ordered Rings and Fields
Autorzy: Schwarzweller, Christoph
Abstrakt: We introduce ordered rings and fields following Artin-Schreier’s approach using positive cones. We show that such orderings coincide with total order relations and give examples of ordered (and non ordered) rings and fields. In particular we show that polynomial rings can be ordered in (at least) two different ways [8, 5, 4, 9]. This is the continuation of the development of algebraic hierarchy in Mizar [2, 3].2017-01-01T00:00:00ZGroup of Homography in Real Projective PlaneCoghetto, Rolandhttp://hdl.handle.net/11320/55692017-10-05T23:14:32Z2017-01-01T00:00:00ZTytuł: Group of Homography in Real Projective Plane
Autorzy: Coghetto, Roland
Abstrakt: Using the Mizar system [2], we formalized that homographies of the projective real plane (as defined in [5]), form a group. Then, we prove that, using the notations of Borsuk and Szmielew in [3] “Consider in space ℝℙ2 points P1, P2, P3, P4 of which three points are not collinear and points Q1,Q2,Q3,Q4 each three points of which are also not collinear. There exists one homography h of space ℝℙ2 such that h(Pi) = Qi for i = 1, 2, 3, 4. ”(Existence Statement 52 and Existence Statement 53) [3]. Or, using notations of Richter [11] “Let [a], [b], [c], [d] in ℝℙ2 be four points of which no three are collinear and let [a′],[b′],[c′],[d′] in ℝℙ2 be another four points of which no three are collinear, then there exists a 3 × 3 matrix M such that [Ma] = [a′], [Mb] = [b′], [Mc] = [c′], and [Md] = [d′] ”Makarios has formalized the same results in Isabelle/Isar (the collineations form a group, lemma statement52-existence and lemma statement 53-existence) and published it in Archive of Formal Proofs [10], [9].2017-01-01T00:00:00ZDifferentiability of Polynomials over RealsKorniłowicz, Arturhttp://hdl.handle.net/11320/55662017-10-05T23:14:29Z2017-01-01T00:00:00ZTytuł: Differentiability of Polynomials over Reals
Autorzy: Korniłowicz, Artur
Abstrakt: In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].2017-01-01T00:00:00Z