DSpace Kolekcja:
http://hdl.handle.net/11320/6815
Fri, 27 Nov 2020 08:58:40 GMT2020-11-27T08:58:40ZDiophantine 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:00ZFubini’s Theorem for Non-Negative or Non-Positive Functions
http://hdl.handle.net/11320/6833
Tytuł: Fubini’s Theorem for Non-Negative or Non-Positive Functions
Autorzy: Endou, Noboru
Abstrakt: The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [10], [2], [3], using the Mizar system [1], [9]. We formalized Fubini’s theorem in our previous article [5], but in that case we showed the Fubini’s theorem for measurable sets and it was not enough as the integral does not appear explicitly.
On the other hand, the theorems obtained in this paper are more general and it can be easily extended to a general integrable function. Furthermore, it also can be easy to extend to functional space Lp [12]. It should be mentioned also that Hölzl and Heller [11] have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there.Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/68332018-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:00ZKlein-Beltrami Model. Part II
http://hdl.handle.net/11320/6832
Tytuł: Klein-Beltrami Model. Part II
Autorzy: Coghetto, Roland
Abstrakt: Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2, 3, 15, 4].
With the Mizar system [1], [10] we use some ideas are taken from Tim Makarios’ MSc thesis [12] for formalized some definitions (like the tangent) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as a further development of Tarski’s geometry in the formal setting [9].Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/11320/68322018-01-01T00:00:00Z