DSpace Kolekcja:
http://hdl.handle.net/11320/6511
2020-11-24T17:23:05ZThe Matiyasevich Theorem. Preliminaries
http://hdl.handle.net/11320/6555
Tytuł: The Matiyasevich Theorem. Preliminaries
Autorzy: Pąk, Karol
Abstrakt: In this article, we prove selected properties of Pell’s equation that are essential to finally prove the Diophantine property of two equations. These equations are explored in the proof of Matiyasevich’s negative solution of Hilbert’s tenth problem.2017-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).2017-01-01T00:00:00ZImplicit Function Theorem. Part I
http://hdl.handle.net/11320/6552
Tytuł: Implicit Function Theorem. Part I
Autorzy: Nakasho, Kazuhisa; Futa, Yuichi; Shidama, Yasunari
Abstrakt: In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit function theorem. In the first section, some composition properties of Lipschitz continuous linear function are discussed. In the second section, a definition of closed ball and theorems of several properties of open and closed sets in Banach space are described. In the last section, we formalized the existence and uniqueness of continuous implicit function in Banach space using Banach fixed point theorem. We referred to [7], [8], and [2] in this formalization.2017-01-01T00:00:00ZIntroduction to Diophantine Approximation. Part II
http://hdl.handle.net/11320/6553
Tytuł: Introduction to Diophantine Approximation. Part II
Autorzy: Watase, Yasushige
Abstrakt: In the article we present in the Mizar system [1], [2] the formalized proofs for Hurwitz’ theorem [4, 1891] and Minkowski’s theorem [5]. Both theorems are well explained as a basic result of the theory of Diophantine approximations appeared in [3], [6]. A formal proof of Dirichlet’s theorem, namely an inequation |θ−y/x| ≤ 1/x2 has infinitely many integer solutions (x, y) where θ is an irrational number, was given in [8]. A finer approximation is given by Hurwitz’ theorem: |θ− y/x|≤ 1/√5x2. Minkowski’s theorem concerns an inequation of a product of non-homogeneous binary linear forms such that |a1x + b1y + c1| · |a2x + b2y + c2| ≤ ∆/4 where ∆ = |a1b2 − a2b1| ≠ 0, has at least one integer solution.2017-01-01T00:00:00Z