Formalized Mathematics    ISSN 1898-9934 (e), ISSN 1426-2630 (p)

 Volume 16, Number 2 (2008): PDF A copy of this issue can also be found on the MetaPress server (with DOI names of articles).

1. Jessica Enright, Piotr Rudnicki. Helly Property for Subtrees, Formalized Mathematics 16(2), pages 91-96, 2008. MML Identifier: HELLY
Summary: We prove, following \cite[p.92]{Golumbic}, that any family of subtrees of a finite tree satisfies the Helly property.
2. Marco Riccardi. Heron's Formula and {P}tolemy's Theorem, Formalized Mathematics 16(2), pages 97-101, 2008. MML Identifier: EUCLID_6
Summary: The goal of this article is to formalize some theorems that are in the \cite{Freek-100-theorems} on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.
3. Hiroyuki Okazaki, Yasunari Shidama. Uniqueness of Factoring an Integer and Multiplicative Group ${\mathbb Z}/p{{\mathbb Z}^\ast}$, Formalized Mathematics 16(2), pages 103-107, 2008. MML Identifier: INT_7
Summary: In the \cite{INT_3.ABS}, it had been proven that the Integers modulo $p$, in this article we shall refer as ${\mathbb Z}/p{\mathbb Z}$, constitutes a field if and only if $p$ is a prime. Then the prime modulo ${\mathbb Z}/p{\mathbb Z}$ is an additive cyclic group and ${\mathbb Z}/p{{\mathbb Z}^\ast}={\mathbb Z}/p{\mathbb Z}\setminus\{0\}$ is a multiplicative cyclic group, too. The former has been proven in the \cite{GR_CY_1.ABS}. However, the latter had not been proven yet. In this article, first, we prove a theorem concerning the LCM to prove the existence of primitive elements of ${\mathbb Z}/p^{\ast}$. Moreover we prove the uniqueness of factoring an integer. Next we define the multiplicative group ${\mathbb Z}/p{{\mathbb Z}^\ast}$ and prove it is cyclic.
4. Chenglong Wu, Yuzhong Ding. Ideals of {BCI}-algebras and their Properties, Formalized Mathematics 16(2), pages 109-114, 2008. MML Identifier: BCIIDEAL
Summary: In this article three classes of ideals are discussed: associative ideals, commutative ideals, implicative ideals and positive implicative ideals, and their elementary properties. Some of their properties and the relationships between them have not been proven yet, and will be completed in the following article.
5. Yasunari Shidama, Hikofumi Suzuki, Noboru Endou. Banach Algebra of Bounded Functionals, Formalized Mathematics 16(2), pages 115-122, 2008. MML Identifier: C0SP1
Summary: In this article, we describe some basic properties of the Banach algebra which is constructed from all bounded functionals.
6. Hidenori Matsuzaki, Noboru Endou, Yasunari Shidama. Convex Sets and Convex Combinations on Complex Linear Spaces, Formalized Mathematics 16(2), pages 123-133, 2008. MML Identifier: CONVEX4
Summary: In this article, convex sets, convex combinations and convex hulls on complex linear spaces are introduced.
7. Fuguo Ge. Inner Products, Group, Ring of Quaternion Numbers, Formalized Mathematics 16(2), pages 135-139, 2008. MML Identifier: QUATERN2
Summary: In this article, we define the division of the quaternion numbers, we also give the definition of inner products, group, ring of the quaternion numbers, and we prove some of their properties.
8. Junjie Zhao, Xiquan Liang, Li Yan. Several Higher Differentiation Formulas of Special Functions, Formalized Mathematics 16(2), pages 141-145, 2008. MML Identifier: HFDIFF_1
Summary: In this paper, we proved some basic properties of higher differentiation, and higher differentiation formulas of special functions \cite{Chen:1978}.
9. Xiquan Liang, Bing Xie. Inverse Trigonometric Functions Arctan and Arccot, Formalized Mathematics 16(2), pages 147-158, 2008. MML Identifier: SIN_COS9
Summary: This article describes definitions of inverse trigonometric functions arctan, arccot and their main properties, as well as several differentiation formulas of arctan and arccot.
10. Bing Xie, Xiquan Liang, Fuguo Ge. Inverse Trigonometric Functions Arcsec and Arccosec, Formalized Mathematics 16(2), pages 159-165, 2008. MML Identifier: SINCOS10
Summary: This article describes definitions of inverse trigonometric functions arcsec and arccosec, as well as their main properties.
11. Noboru Endou, Keiko Narita, Yasunari Shidama. The {L}ebesgue Monotone Convergence Theorem, Formalized Mathematics 16(2), pages 167-175, 2008. MML Identifier: MESFUNC9
12. Grzegorz Bancerek. Mizar Analysis of Algorithms: Algorithms over Integers, Formalized Mathematics 16(2), pages 177-194, 2008. MML Identifier: AOFA_I00
Summary: This paper is a continuation of \cite{AOFA_000.ABS} and concerns if-while algebras over integers. In these algebras the only elementary instructions are assignment instructions. The instruction assigns to a (program) variable a value which is calculated for the current state according to some arithmetic expression. The expression may include variables, constants, and a limited number of arithmetic operations. States are functions from a given set of locations into integers. A variable is a function from the states into the locations and an expression is a function from the states into integers. Additional conditions (computability) limit the set of variables and expressions and, simultaneously, allow to write algorithms in a natural way (and to prove their correctness).\par As examples the proofs of full correctness of two Euclid algorithms (with modulo operation and subtraction) and algorithm of exponentiation by squaring are given.
13. Yatsuka Nakamura, Kunio Oniumi, Wenpai Chang. Invertibility of Matrices of Field Elements, Formalized Mathematics 16(2), pages 195-202, 2008. MML Identifier: MATRIX14
Summary: In this paper the theory of invertibility of matrices of field elements (see e.g. \cite{Furuya:57}, \cite{Gantmacher:59}) is developed. The main purpose of this article is to prove that the left invertibility and the right invertibility are equivalent for a matrix of field elements. To prove this, we introduced a special transformation of matrix to some canonical forms. Other concepts as zero vector and base vectors of field elements are also introduced as a preparation.
14. Marco Riccardi. Ramsey's Theorem, Formalized Mathematics 16(2), pages 203-205, 2008. MML Identifier: RAMSEY_1
Summary: The goal of this article is to formalize two versions of Ramsey's theorem. The theorems are not phrased in the usually pictorial representation of a coloured graph but use a set-theoretic terminology. After some useful lemma, the second section presents a generalization of Ramsey's theorem on infinite set closely following the book \cite{ThomasJech2002}. The last section includes the formalization of the theorem in a more known version (see \cite{PFTB}).
15. Grzegorz Bancerek. Towards the Construction of a Model of {M}izar Concepts, Formalized Mathematics 16(2), pages 207-230, 2008. MML Identifier: ABCMIZ_1
Summary: The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from \cite{Bancerek:2003} and \cite{ABCMIZ_0.ABS}. The theory here presented is an abstract of the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The base idea behind the formalization is dependence on variables which is determined by variable-dependence (variables may depend on other variables). The dependence constitutes a Galois connection between opposite poset of dependence-closed set of variables and the sup-semilattice of widening of Mizar types (smooth type widening).\par In the paper the concepts strictly connected with Mizar expressions are formalized. Among them are quasi-loci, quasi-terms, quasi-adjectives, and quasi-types. The structural induction and operation of substitution are also introduced. The prefix {\it quasi} is used to indicate that some rules of construction of Mizar expressions may not be fulfilled. For example, variables, quasi-loci, and quasi-terms have no assigned types and, in result, there is no possibility to conduct type-checking of arguments. The other gaps concern inconsistent and out-of-context clusters of adjectives in types. Those rules are required in the Mizar {\it identification} process. However, the expression appearing in later processes of Mizar checker may not satisfy the rules. So, introduced apparatus is enough and adequate to describe data structures and algorithms from the Mizar checker (like {\it equational classes}).