A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Kazuhisa Ishida.
Model Checking. {P}art {II},
Formalized Mathematics 16(3),
pages 231-245, 2008. MML Identifier:
MODELC_2 Summary:
This article provides the definition of linear temporal logic (LTL) and its properties
relevant to model checking based on
\cite{Clarke2000}.
Mizar formalization of LTL language and satisfiability is based on
\cite{ZF_LANG.ABS,
ZF_MODEL.ABS}.
Christoph Schwarzweller.
Modular Integer Arithmetic,
Formalized Mathematics 16(3),
pages 247-252, 2008. MML Identifier:
INT_6 Summary:
In this article we show the correctness of integer arithmetic
based on Chinese Remainder theorem as described e.g. in
\cite{ModernComputerAlgebra}:
Integers are transformed to finite
sequences of modular integers, on which the arithmetic operations
are performed. Retransformation of the results to the integers is
then accomplished by means of the Chinese Remainder theorem.
The method presented is a typical example for computing in
homomorphic images.
Tao Sun, Weibo Pan, Chenglong Wu, Xiquan Liang.
General Theory of Quasi-Commutative {BCI}-algebras,
Formalized Mathematics 16(3),
pages 253-258, 2008. MML Identifier:
BCIALG_5 Summary:
It is known that commutative BCK-algebras form a variety,
but BCK-algebras do not
\cite{BCIAlgebras}.
Therefore H.Yutani introduced the notion
of quasi-commutative BCK-algebras. In this article we first
present the notion and general theory of quasi-commutative BCI-algebras.
Then we discuss the reduction of the type of quasi-commutative
BCK-algebras and some special classes of quasi-commutative BCI-algebras.
Karol P\k{a}k.
Block Diagonal Matrices,
Formalized Mathematics 16(3),
pages 259-267, 2008. MML Identifier:
MATRIXJ1 Summary:
In this paper I present basic properties of block diagonal
matrices over a set. In my approach the finite sequence of
matrices in a block diagonal matrix is not restricted to square
matrices. Moreover, the off-diagonal blocks need not be zero
matrices, but also with another arbitrary fixed value.
Karol P\k{a}k.
Linear Map of Matrices,
Formalized Mathematics 16(3),
pages 269-275, 2008. MML Identifier:
MATRLIN2 Summary:
The paper is concerned with a generalization of concepts introduced in
\cite{MATRLIN.ABS},
i.e. introduced are matrices of linear
transformations over a finite-dimensional vector space.
Introduced are linear transformations over a finite-dimensional
vector space depending on a given matrix of the transformation.
Finally, I prove that the rank of linear transformations over a
finite-dimensional vector space is the same as the rank of the
matrix of that transformation.
El\.zbieta M\k{a}dra, Adam Grabowski.
Orthomodular Lattices,
Formalized Mathematics 16(3),
pages 277-282, 2008. MML Identifier:
ROBBINS4 Summary:
The main result of the article is the solution to the problem
of short axiomatizations of orthomodular ortholattices.
Based on EQP/Otter results
\cite{McCune:2005}, we gave a set of
three equations which is equivalent to the classical, much longer
equational basis of such a class. Also the basic example of the
lattice which is not orthomodular, i.e. benzene (or $B_6$) is
defined in two settings -- as a relational structure (poset) and
as a lattice. \par As a preliminary work, we present the proofs of
the dependence of other axiomatizations of ortholattices. The
formalization of the properties of orthomodular lattices follows
\cite{Beran:1984}.
Yatsuka Nakamura, Hisashi Ito.
Basic Properties and Concept
of Selected Subsequence of Zero Based Finite Sequences,
Formalized Mathematics 16(3),
pages 283-288, 2008. MML Identifier:
AFINSQ_2 Summary:
Here, we develop the theory of zero based finite sequences,
which are sometimes, more useful in applications than normal
one based finite sequences. The fundamental function Sgm is
introduced as well as in case of normal finite sequences and
other notions are also introduced. However, many theorems are
a modification of old theorems of normal finite sequences,
they are basically important and are necessary for applications.
A new concept of selected subsequence is introduced. This concept
came from the individual Ergodic theorem (see
\cite{Halmos:1956})
and it is the preparation for its proof.