DSpace Kolekcja: http://hdl.handle.net/11320/6511 2020-11-29T23:13:41Z 2020-11-29T23:13:41Z The Matiyasevich Theorem. Preliminaries Pąk, Karol http://hdl.handle.net/11320/6555 2018-05-25T10:23:32Z 2017-01-01T00:00:00Z Tytu&#322;: 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:00Z Tarski Geometry Axioms. Part III Coghetto, Roland Grabowski, Adam http://hdl.handle.net/11320/6554 2018-05-14T08:16:15Z 2017-01-01T00:00:00Z Tytu&#322;: 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:00Z Implicit Function Theorem. Part I Nakasho, Kazuhisa Futa, Yuichi Shidama, Yasunari http://hdl.handle.net/11320/6552 2018-05-14T08:24:50Z 2017-01-01T00:00:00Z Tytu&#322;: Implicit Function Theorem. Part I Autorzy: Nakasho, Kazuhisa; Futa, Yuichi; Shidama, Yasunari Abstrakt: In this article, we formalize in Mizar ,  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 , , and  in this formalization. 2017-01-01T00:00:00Z Introduction to Diophantine Approximation. Part II Watase, Yasushige http://hdl.handle.net/11320/6553 2018-05-14T08:07:37Z 2017-01-01T00:00:00Z Tytu&#322;: Introduction to Diophantine Approximation. Part II Autorzy: Watase, Yasushige Abstrakt: In the article we present in the Mizar system ,  the formalized proofs for Hurwitz’ theorem [4, 1891] and Minkowski’s theorem . Both theorems are well explained as a basic result of the theory of Diophantine approximations appeared in , . 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 . 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