A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
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.
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.
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.
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.
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.
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.
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.
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}.
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.
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.
Noboru Endou, Keiko Narita, Yasunari Shidama.
The {L}ebesgue Monotone Convergence Theorem,
Formalized Mathematics 16(2),
pages 167-175, 2008. MML Identifier:
MESFUNC9 Summary:
In this article we prove the Monotone Convergence Theorem
\cite{Halmos74}.
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.
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.
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}).
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}).