All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Page 1 Next

Displaying 1 – 20 of 22

Showing per page

Taclets: a new paradigm for constructing interactive theorem provers.

Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager (2004)

RACSAM

Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...

Tarski Geometry Axioms – Part II

Roland Coghetto, Adam Grabowski (2016)

Formalized Mathematics

In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation), of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1), congruence equivalence relation (A2), congruence identity (A3), segment construction (A4), SAS (A5), betweenness...

The Axiomatization of Propositional Logic

Mariusz Giero (2016)

Formalized Mathematics

This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows φ ::= ⊥ | p | φ → φ. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes α ⇒ (β ⇒ α), (α ⇒ (β ⇒ γ)) ⇒ ((α ⇒ β) ⇒ (α ⇒ γ)), (¬β ⇒ ¬α) ⇒ ((¬β ⇒ α) ⇒ β). Modus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved....

The Basic Existence Theorem of Riemann-Stieltjes Integral

Kazuhisa Nakasho, Keiko Narita, Yasunari Shidama (2016)

Formalized Mathematics

In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15],...

The First Isomorphism Theorem and Other Properties of Rings

Artur Korniłowicz, Christoph Schwarzweller (2014)

Formalized Mathematics

Different properties of rings and fields are discussed [12], [41] and [17]. We introduce ring homomorphisms, their kernels and images, and prove the First Isomorphism Theorem, namely that for a homomorphism f : R → S we have R/ker(f) ≅ Im(f). Then we define prime and irreducible elements and show that every principal ideal domain is factorial. Finally we show that polynomial rings over fields are Euclidean and hence also factorial

The First Mean Value Theorem for Integrals

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.MML identifier: MESFUNC7, version: 7.8.09 4.97.1001

The Formal Construction of Fuzzy Numbers

Adam Grabowski (2014)

Formalized Mathematics

In this article, we continue the development of the theory of fuzzy sets [23], started with [14] with the future aim to provide the formalization of fuzzy numbers [8] in terms reflecting the current state of the Mizar Mathematical Library. Note that in order to have more usable approach in [14], we revised that article as well; some of the ideas were described in [12]. As we can actually understand fuzzy sets just as their membership functions (via the equality of membership function and their set-theoretic...

The Formalization of Decision-Free Petri Net

Pratima K. Shah, Pauline N. Kawamoto, Mariusz Giero (2014)

Formalized Mathematics

In this article we formalize the definition of Decision-Free Petri Net (DFPN) presented in [19]. Then we formalize the concept of directed path and directed circuit nets in Petri nets to prove properties of DFPN. We also present the definition of firing transitions and transition sequences with natural numbers marking that always check whether transition is enabled or not and after firing it only removes the available tokens (i.e., it does not remove from zero number of tokens). At the end of this...

The Lebesgue Monotone Convergence Theorem

Noboru Endou, Keiko Narita, Yasunari Shidama (2008)

Formalized Mathematics

In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011

The Linearity of Riemann Integral on Functions from ℝ into Real Banach Space

Keiko Narita, Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

In this article, we described basic properties of Riemann integral on functions from R into Real Banach Space. We proved mainly the linearity of integral operator about the integral of continuous functions on closed interval of the set of real numbers. These theorems were based on the article [10] and we referred to the former articles about Riemann integral. We applied definitions and theorems introduced in the article [9] and the article [11] to the proof. Using the definition of the article [10],...

The Measurability of Complex-Valued Functional Sequences

Keiko Narita, Noboru Endou, Yasunari Shidama (2009)

Formalized Mathematics

In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued functional sequences. Next, we defined complex-valued functional sequences dividing real part into imaginary part. Then using the former theorems, we proved the measurability of each part. Lastly, we proved the measurability of the limits of complex-valued functional sequences. We also showed several properties of complex-valued measurable functions....

The Orthogonal Projection and the Riesz Representation Theorem

Keiko Narita, Noboru Endou, Yasunari Shidama (2015)

Formalized Mathematics

In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals...

Tietze Extension Theorem for n-dimensional Spaces

Karol Pąk (2014)

Formalized Mathematics

In this article we prove the Tietze extension theorem for an arbitrary convex compact subset of εn with a non-empty interior. This theorem states that, if T is a normal topological space, X is a closed subset of T, and A is a convex compact subset of εn with a non-empty interior, then a continuous function f : X → A can be extended to a continuous function g : T → εn. Additionally we show that a subset A is replaceable by an arbitrary subset of a topological space that is homeomorphic with a convex...

Topological Interpretation of Rough Sets

Adam Grabowski (2014)

Formalized Mathematics

Rough sets, developed by Pawlak, are an important model of incomplete or partially known information. In this article, which is essentially a continuation of [11], we characterize rough sets in terms of topological closure and interior, as the approximations have the properties of the Kuratowski operators. We decided to merge topological spaces with tolerance approximation spaces. As a testbed for our developed approach, we restated the results of Isomichi [13] (formalized in Mizar in [14]) and...

Topological Properties of Real Normed Space

Kazuhisa Nakasho, Yuichi Futa, Yasunari Shidama (2014)

Formalized Mathematics

In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered...

Topology from Neighbourhoods

Roland Coghetto (2015)

Formalized Mathematics

Using Mizar [9], and the formal topological space structure (FMT_Space_Str) [19], we introduce the three U-FMT conditions (U-FMT filter, U-FMT with point and U-FMT local) similar to those VI, VII, VIII and VIV of the proposition 2 in [10]: If to each element x of a set X there corresponds a set B(x) of subsets of X such that the properties VI, VII, VIII and VIV are satisfied, then there is a unique topological structure on X such that, for each x ∈ X, B(x) is the set of neighborhoods of x in this...

Torsion Part of ℤ-module

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2015)

Formalized Mathematics

In this article, we formalize in Mizar [7] the definition of “torsion part” of ℤ-module and its properties. We show ℤ-module generated by the field of rational numbers as an example of torsion-free non free ℤ-modules. We also formalize the rank-nullity theorem over finite-rank free ℤ-modules (previously formalized in [1]). ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [23] and cryptographic systems with lattices [24].

Currently displaying 1 – 20 of 22

Page 1 Next