Loading [MathJax]/extensions/MathZoom.js
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...
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...
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....
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],...
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
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
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...
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...
In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011
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],...
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....
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...
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...
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...
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...
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...
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