VOLUME 11, NUMBER 3 (2003), Formalized Mathematics, ISSN 1898-9934 (Online), ISSN 1426-2630 (Print)

Formalized Mathematics (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 11, Number 3 (2003): pdf, ps, dvi.

Yatsuka Nakamura. General Fashoda Meet Theorem for Unit Circle and Square, Formalized Mathematics 11(3), pages 213-224, 2003. MML Identifier: JGRAPH_6
Summary: Here we will prove Fashoda meet theorem for the unit circle and for a square, when 4 points on the boundary are ordered cyclically. Also, the concepts of general rectangle and general circle are defined.
Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, Yasunari Shidama. On Some Properties of Real Hilbert Space. Part I, Formalized Mathematics 11(3), pages 225-229, 2003. MML Identifier: BHSP_6
Summary: In this paper, we first introduce the notion of summability of an infinite set of vectors of real Hilbert space, without using index sets. Further we introduce the notion of weak summability, which is weaker than that of summability. Then, several statements for summable sets and weakly summable ones are proved. In the last part of the paper, we give a necessary and sufficient condition for summability of an infinite set of vectors of real Hilbert space as our main theorem. The last theorem is due to \cite{Halmos87}.
Shin'nosuke Yamaguchi, Grzegorz Bancerek, Katsumi Wasaki. Full Subtracter Circuit. Part II, Formalized Mathematics 11(3), pages 231-236, 2003. MML Identifier: FSCIRC_2
Summary: In this article we continue investigations from \cite{FSCIRC_1.ABS} of verification of a design of subtracter circuit. We define it as a combination of multi cell circuit using schemes from \cite{CIRCCMB2.ABS}. As the main result we prove the stability of the circuit.
Jing-Chao Chen. Dijkstra's Shortest Path Algorithm, Formalized Mathematics 11(3), pages 237-247, 2003. MML Identifier: GRAPHSP
Summary: The article formalizes Dijkstra's shortest path algorithm \cite{Dijkstra59}. A path from a source vertex $v$ to $a$ target vertex $u$ is said to be the shortest path if its total cost is minimum among all $v$-to-$u$ paths. Dijkstra's algorithm is based on the following assumptions: \begin{itemize} \item All edge costs are non-negative. \item The number of vertices is finite. \item The source is a single vertex, but the target may be all other vertices. \end{itemize} The underlying principle of the algorithm may be described as follows: the algorithm starts with the source; it visits the vertices in order of increasing cost, and maintains a set $V$ of visited vertices (denoted by UsedVx in the article) whose cost from the source has been computed, and a tentative cost $D(u)$ to each unvisited vertex $u.$ In the article, the set of all unvisited vertices is denoted by UnusedVx. $D(u)$ is the cost of the shortest path from the source to u in the subgraph induced by $V \cup \{u\}.$ We denote the set of all unvisited vertices whose $D$-values are not infinite (i.e. in the subgraph each of which has a path from the source to itself) by OuterVx. Dijkstra's algorithm repeatedly searches OuterVx for the vertex with minimum tentative cost (this procedure is called findmin in the article), adds it to the set $V$ and modifies $D$-values by a procedure, called Relax. Suppose the unvisited vertex with minimum tentative cost is $x$, the procedure Relax replaces $D(u)$ with min$\{D(u),D(u)+cost(x,u)\}$ where $u$ is a vertex in UnusedVx, and cost$(x,u)$ is the cost of edge $(x,u).$ In the Mizar library, there are several computer models, e.g. SCMFSA and SCMPDS etc. However, it is extremely difficult to use these models to formalize the algorithm. Instead, we adopt functions in the Mizar library, which seem to be pseudo-codes, and are similar to those in the functional programming language, e.g. Lisp. To date, there is no rigorous justification with respect to the correctness of Dijkstra's algorithm. The article presents first the rigorous justification.
Noboru Endou, Yasumasa Suzuki, Yasunari Shidama. Real Linear Space of Real Sequences, Formalized Mathematics 11(3), pages 249-253, 2003. MML Identifier: RSSPACE
Summary: The article is a continuation of \cite{RLVECT_1.ABS}. As the example of real linear spaces, we introduce the arithmetic addition in the set of real sequences and also introduce the multiplication. This set has the arithmetic structure which depends on these arithmetic operations.
Noboru Endou, Yasumasa Suzuki, Yasunari Shidama. Hilbert Space of Real Sequences, Formalized Mathematics 11(3), pages 255-257, 2003. MML Identifier: RSSPACE2
Summary: A continuation of \cite{RLVECT_1.ABS}. As the example of real unitary spaces, we introduce the arithmetic addition and multiplication in the set of square sum able real sequences and introduce the scaler products also. This set has the structure of the Hilbert space.
Takao Inoue. Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part I, Formalized Mathematics 11(3), pages 259-266, 2003. MML Identifier: INTPRO_1
Summary: In this paper, we develop intuitionistic propositional calculus IPC in the extended language with single modal operator. The formulation that we adopt in this paper is very useful not only to formalize the calculus but also to do a number of logics with essentially propositional character. In addition, it is much simpler than the past formalization for modal logic. In the first section, we give the mentioned formulation which the author heavily owes to the formalism of Adam Grabowski's \cite{HILBERT1.ABS}. After the theoretical development of the logic, we prove a number of valid formulas of IPC in the sections 2--4. The last two sections are devoted to present classical propositional calculus and modal calculus S4 in our framework, as a preparation for future study. In the forthcoming Part II of this paper, we shall prove, among others, a number of intuitionistically valid formulas with negation.
Noboru Endou, Yasumasa Suzuki, Yasunari Shidama. Some Properties for Convex Combinations, Formalized Mathematics 11(3), pages 267-270, 2003. MML Identifier: CONVEX2
Summary: This is a continuation of \cite{CONVEX1.ABS}. In this article, we proved that convex combination on convex family is convex.
Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inoue, Yasunari Shidama. On Some Properties of Real Hilbert Space. Part II, Formalized Mathematics 11(3), pages 271-273, 2003. MML Identifier: BHSP_7
Summary: This paper is a continuation of our paper \cite{BHSP_6.ABS}. We give an analogue of the necessary and sufficient condition for summable set (i.e. the main theorem of \cite{BHSP_6.ABS}) with respect to summable set by a functional $L$ in real Hilbert space. After presenting certain useful lemmas, we prove our main theorem that the summability for an orthonormal infinite set in real Hilbert space is equivalent to its summability with respect to the square of norm, say $H(x) = (x, x)$. Then we show that the square of norm $H$ commutes with infinite sum operation if the orthonormal set under our consideration is summable. Our main theorem is due to \cite{Halmos87}.
Wenpai Chang, Yatsuka Nakamura, Piotr Rudnicki. Inner Products and Angles of Complex Numbers, Formalized Mathematics 11(3), pages 275-280, 2003. MML Identifier: COMPLEX2
Summary: An inner product of complex numbers is defined and used to characterize the (counter-clockwise) angle between ($a$,0) and (0,$b$) in the complex plane. For complex $a$, $b$ and $c$ we then define the (counter-clockwise) angle between ($a$,$c$) and ($c$, $b$) and prove theorems about the sum of internal and external angles of a triangle.
Akihiro Kubo, Yatsuka Nakamura. Angle and Triangle in Euclidian Topological Space, Formalized Mathematics 11(3), pages 281-287, 2003. MML Identifier: EUCLID_3
Summary: Two transformations between the complex space and 2-dimensional Euclidian topological space are defined. By them, the concept of argument is induced to 2-dimensional vectors using argument of complex number. Similarly, the concept of an angle is introduced using the angle of two complex numbers. The concept of a triangle and related concepts are also defined in $n$-dimensional Euclidian topological spaces.
Krzysztof Retel. The Class of Series-Parallel Graphs. Part II, Formalized Mathematics 11(3), pages 289-291, 2003. MML Identifier: NECKLA_2
Summary: In this paper we introduce two new operations on graphs: sum and union corresponding to parallel and series operation respectively. We determine $N$-free graph as the graph that does not embed Necklace $4$. We define ``fin\_RelStr" as the set of all graphs with finite carriers. We also define the smallest class of graphs which contains the one-element graph and which is closed under parallel and series operations. The goal of the article is to prove the theorem that the class of finite series-parallel graphs is the class of finite $N$-free graphs. This paper formalizes the next part of \cite{Thomasse}.
Christoph Schwarzweller. Characterization and Existence of Gr\"obner Bases, Formalized Mathematics 11(3), pages 293-301, 2003. MML Identifier: GROEB_1
Summary: We continue the Mizar formalization of Gr\"{o}bner bases following \cite{Becker93}. In this article we prove a number of characterizations of Gr\"{o}bner bases among them that Gr\"{o}bner bases are convergent rewriting systems. We also show the existence and uniqueness of reduced Gr\"{o}bner bases.
Christoph Schwarzweller. Construction of Gr\"obner bases. S-Polynomials and Standard Representations, Formalized Mathematics 11(3), pages 303-312, 2003. MML Identifier: GROEB_2
Summary: We continue the Mizar formalization of Gr\"{o}bner bases following \cite{Becker93}. In this article we introduce S-polynomials and standard representations and show how these notions can be used to characterize Gr\"{o}bner bases.
Adam Grabowski. On the Subcontinua of a Real Line, Formalized Mathematics 11(3), pages 313-322, 2003. MML Identifier: BORSUK_5
Summary: In \cite{BORSUK_4.ABS} we showed that the only proper subcontinua of the simple closed curve are arcs and single points. In this article we prove that the only proper subcontinua of the real line are closed intervals. We introduce some auxiliary notions such as $\rbrack a,b\lbrack_{\Bbb Q}$, $\rbrack a,b\lbrack_{\Bbb I\Bbb Q}$ -- intervals consisting of rational and irrational numbers respectively. We show also some basic topological properties of intervals.
Lilla Krystyna Baginska, Adam Grabowski. On the Kuratowski Closure-Complement Problem, Formalized Mathematics 11(3), pages 323-329, 2003. MML Identifier: KURATO_1
Summary: In this article we formalize the Kuratowski closure-complement result: there is at most 14 distinct sets that one can produce from a given subset $A$ of a topological space $T$ by applying closure and complement operators and that all 14 can be obtained from a suitable subset of $\Bbb R,$ namely KuratExSet $=\{1\} \cup {\Bbb Q} (2,3) \cup (3, 4)\cup (4,\infty)$.\par The second part of the article deals with the maximal number of distinct sets which may be obtained from a given subset $A$ of $T$ by applying closure and interior operators. The subset KuratExSet of $\Bbb R$ is also enough to show that 7 can be achieved.
Noboru Endou, Yasunari Shidama. Convex Hull, Set of Convex Combinations and Convex Cone, Formalized Mathematics 11(3), pages 331-333, 2003. MML Identifier: CONVEX3
Summary: In this article, there are two themes. One of them is the proof that convex hull of a given subset $M$ consists of all convex combinations of $M.$ Another is definitions of cone and convex cone and some properties of them.
Wioletta Truszkowska, Adam Grabowski. On the Two Short Axiomatizations of Ortholattices, Formalized Mathematics 11(3), pages 335-340, 2003. MML Identifier: ROBBINS2
Summary: In the paper, two short axiom systems for Boolean algebras are introduced. In the first section we show that the single axiom (DN${}_1$) proposed in \cite{McCune:2001} in terms of disjunction and negation characterizes Boolean algebras. To prove that (DN${}_1$) is a single axiom for Robbins algebras (that is, Boolean algebras as well), we use the Otter theorem prover. The second section contains proof that the two classical axioms (Meredith${}_1$), (Meredith${}_2$) proposed by Meredith \cite{Meredith:1968} may also serve as a basis for Boolean algebras. The results will be used to characterize ortholattices.