A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Krzysztof Treyderowski, Christoph Schwarzweller.
Multiplication of Polynomials using Discrete Fourier Transformation,
Formalized Mathematics 14(4), pages 121-128, 2006. MML Identifier: POLYNOM8 Summary: In this article we define the Discrete Fourier Transformation for univariate polynomials and show that multiplication of polynomials can be carried out by two Fourier Transformations with a vector multiplication inbetween. Our proof follows the standard one found in the literature and uses Vandermonde matrices, see e.g. \cite{ModernComputerAlgebra}.
Xiquan Liang, Fuguo Ge, Xiaopeng Yue.
Some Special Matrices of Real Elements and Their Properties,
Formalized Mathematics 14(4), pages 129-134, 2006. MML Identifier: MATRIX10 Summary: This article describes definitions of positive matrix, negative matrix, nonpositive matrix, nonnegative matrix, nonzero matrix, module matrix of real elements and their main properties, and we also give the basic inequalities in matrices of real elements.
Christoph Schwarzweller, Agnieszka Rowinska-Schwarzweller.
Schur's Theorem on the Stability of Networks,
Formalized Mathematics 14(4), pages 135-142, 2006. MML Identifier: HURWITZ Summary: A complex polynomial is called a Hurwitz polynomial, if all its roots have a real part smaller than zero. This kind of polynomial plays an all-dominant role in stability checks of electrical networks.\par In this article we prove Schur's criterion \cite{SCHUR:1} that allows to decide whether a polynomial $p(x)$ is Hurwitz without explicitely computing its roots: Schur's recursive algorithm successively constructs polynomials $p_i(x)$ of lesser degree by division with $x-c$, $\Re\{c\} < 0$.
Yasunari Shidama, Noboru Endou.
Integral of Real-Valued Measurable Function,
Formalized Mathematics 14(4), pages 143-152, 2006. MML Identifier: MESFUNC6 Summary: Based on \cite{Halmos}, authors formalized the integral of an extended real valued measurable function in \cite{MESFUNC5.ABS} before. However, the integral argued in \cite{MESFUNC5.ABS} cannot be applied to real-valued functions unconditionally. Therefore we formalized the integral of a real-value function in this article.
Karol Pcak.
The Catalan Numbers. Part II,
Formalized Mathematics 14(4), pages 153-159, 2006. MML Identifier: CATALAN2 Summary: In this paper, we define sequence dominated by $0$, in which every initial fragment contains more zeroes than ones. If $n \geq 2 \cdot m$ and $n>0$, then the number of sequences dominated by $0$ the length $n$ including $m$ of ones, is given by the formula $$D(n,m)=\frac{n+1-2\cdot m}{n+1-m}\cdot{n \choose m}$$ and satisfies the recurrence relation $$D(n,m)=D(n-1,m)\:+\:\sum_{i=0}^{m-1} D(2\cdot i,i)\cdot D(n-2\cdot(i+1),m - (i+1)).$$ Obviously, if $n = 2 \cdot m$, then we obtain the recurrence relation for the Catalan numbers (starting from $0$) $$C_{m+1}=\sum_{i=0}^{m-1} C_{i+1}\cdot C_{m-i}.$$ Using the above recurrence relation we can see that $$\sum_{i=0}^\infty\,C_{i+1}\cdot x^i\,= \,1\,+\,\left(\sum_{i=0}^\infty\, C_{i+1}\cdot x^i\right)^2$$ where ($| x |< \frac{1}{4}$) and hence $$\sum_{i=0}^\infty\, C_{i+1}\cdot x^i\,= \,\frac{1-\sqrt[]{1-4\cdot x}}{2\cdot x}.$$
Xiquan Liang, Fuguo Ge.
The Quaternion Numbers,
Formalized Mathematics 14(4), pages 161-169, 2006. MML Identifier: QUATERNI Summary: In this article, we define the set $\Bbb Q$ of quaternion numbers as the set of all ordered sequences $q =\langle x,y,w,z\rangle$ where $x$,$y$,$w$ and $z$ are real numbers. The addition, difference and multiplication of the quaternion numbers are also defined. We define the real and imaginary parts of $q$ and denote this by $x = \Rea(q)$, $y = \Im1(q)$, $w = \Im2(q)$, $z = \Im3(q)$. We define the addition, difference, multiplication again and denote this operation by real and three imaginary parts. We define the conjugate of $q$ denoted by $q*'$ and the absolute value of $q$ denoted by $|.q.|$. We also give some properties of quaternion numbers.
Kazuhisa Ishida.
Model Checking. Part I,
Formalized Mathematics 14(4), pages 171-186, 2006. MML Identifier: MODELC_1 Summary: This text includes definitions of the Kripke structure, CTL (Computation Tree Logic), and verification of the basic algorithm for Model Checking based on CTL. Text book for reference: Model Checking, E. M. Clarke, Orna Grumberg, Doron Peled, Mit Pr (2000/1/7)
Broderick Arneson, Piotr Rudnicki.
Recognizing Chordal Graphs: Lex BFS and MCS,
Formalized Mathematics 14(4), pages 187-205, 2006. MML Identifier: LEXBFS Summary: We are formalizing the algorithm for recognizing chordal graphs by lexicographic breadth-first search as presented in \cite[Section 3 of Chapter4, pp.~81--84]{Golumbic}. Then we follow with a formalization of another algorithm serving the same end but based on maximum cardinality search as presented by Tarjan and Yannakakis~\cite{TY84}.\par This work is a part of the MSc work of the first author under supervision of the second author. We would like to thank one of the anonymous reviewers for very useful suggestions.
Noboru Endou, Yasunari Shidama, Katsumasa Okamura.
Baire's Category Theorem and Some Spaces Generated from Real Normed Space,
Formalized Mathematics 14(4), pages 213-219, 2006. MML Identifier: NORMSP_2 Summary: As application of complete metric space, we proved a Baire's category theorem. Then we defined some spaces generated from real normed space and discussed about each. In the second section we showed an equivalence of convergence and a continuity of a function. In other sections, we showed some topological properties of two spaces, which are topological space and linear topological space generated from real normed space.
Adam Naumowicz.
On the Representation of Natural Numbers in Positional Numeral Systems,
Formalized Mathematics 14(4), pages 221-223, 2006. MML Identifier: NUMERAL1 Summary: In this paper we show that every natural number can be uniquely represented as a base-$b$ numeral. The formalization is based on the proof presented in \cite{SIERPINSKI:1}. We also prove selected divisibility criteria in the base-$10$ numeral system.
Bo Zhang, Hiroshi Yamazaki and Yatsuka Nakamura.
The Relevance of Measure and Probability, and Definition of Completeness of Probability,
Formalized Mathematics 14(4), pages 225-229, 2006. MML Identifier: PROB_4 Summary: In this article, we first discuss the relation between measure defined using extended real numbers and probability defined using real numbers. Further, we define completeness of probability, and its completion method, and also show that they coincide with those of measure.