Calculemus
System for Integrated Computation and Deduction
funded under the 5th Framework Programme of the European Commission
Contract Reference HPRNCT200000102
MIZAR Group
University of Bialystok


Description of the Scientific Progress and Networking
People
Active visiting researchers
Josef Urban (Charles University). Young visiting researcher
at University of Bialystok from 02/2002 to 08/2002.
Josef's work consists of designing an XML format for the
Mizar system,
that would enable various presentation and export functions for the
Mizar Mathematical Library.
Another task is exploring the Mizar type system
and formalizing related type theories in Mizar. Josef contributed
5 Mizar articles to Mizar Mathematical Library devoted to the theory of order sorted algebras:

Order Sorted Algebras,
Journal of Formalized Mathematics, Vol. 14.

Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras,
Journal of Formalized Mathematics, Vol. 14.

Homomorphisms of Order Sorted Algebras,
Journal of Formalized Mathematics, Vol. 14.

Order Sorted Quotient Algebra,
Journal of Formalized Mathematics, Vol. 14.

Free Order Sorted Universal Algebra,
Journal of Formalized Mathematics, Vol. 14.
Artur Kornilowicz (University of Bialystok). Young visiting researcher at IRST from 16/07/2001 to 30/06/2002.
Research activities
The Mizar research group at the University of Bialystok
is involved in the following tasks of the Calculemus project:
 Task 3.1 Automated support to writing mathematical publications
UwB's contribution to this task consists in maintaining the technology adopted for publishing
Mizar articles. The automated support for writing and publishing Mizar articles consists of:
 The software used for writing and checking the correctness of Mizar articles
(http://mizar.org/system/)
 The software used for automatic translation and typesetting of the exportable parts of Mizar
articles are automatically translated into English and organized as a LaTeX source.
The resulting papers are first published electronically
(http://mizar.org/JFM/), and then the paper edition follows
(Formalized Mathematics, ISSN 14262630, published since 1990).
The plan for future:
Both parts of the software are still evolving. The first part (the system for checking
Mizar articles) will be made stronger. That will enable writing proofs with the length closer
to the length of proofs in informal mathematical publications. Nowadays, the de Bruijn factor for
Mizar articles ranges beteween 3 and 4. The second part (the system producing LaTeX output) will
be extended to provide better description of the environment in which articles are written and
to enable publication of proofs, probably after compression.
Recently, an attempt to create
Encyclopedia of Mathematics in Mizar was initiated. Encyclopedic articles are supposed to comprehensively cover selected areas of mathematics.
 Task 3.4 Modelling of existing systems as Mathematical Services
UwB's contribution to this task consists of:
 Maintaining and developing the hyperlinked collection of abstracts of all articles
collected in the Mizar Mathematical Library.
All concepts used in Mizar articles are linked to their definitions. This service
is frequently used by many Mizar authors. It is also possible to use it offline
(ftp://mizar.uwb.edu.pl/pub/jfm/jfmabstr.tar.gz).
 An experiment with distant learning through Internet has been completed
(so called 'Hagenberg Course' of Mizar for students from THEOREMA group (RISC)).
It lasted from January 07 till March 05, 2002. In that period Hagenberg students
solved 35 quite advanced exercises.
 Remote Mizar course has been included in SUGSI
 Graduate School of Science and Technology on the Internet at
Shinshu University.
 Closely related to the topic is the work done in Japan consisting of:
 Task 3.5 Challenge mathematical problems
UwB's research in this task concerns mainly:
The research within Calculemus tasks stimulated the following evolution of Mizar system:
 redesign of the implementation of 'attributes'
 implementation of new 'requirements' directives (BOOLE, REAL)
 introducing new 'properties' for binary (idempotence) and unary (involutiveness, projectivity) functors
 theoretical modeling of the Mizar type system  dependent types
algebras.
Networking
Joint publications

Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto
Sebastiani
"Bounded Model Checking for Timed Systems."
In Proc. 22nd Joint International Conference on Formal
Techniques for Networked and Distributed Systems (FORTE 2002).
Houston, TX, USA, November 2002.
LNCS
©
Springer Verlag.

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur
Kornilowicz, Roberto Sebastiani
"A SAT Based Approach for Solving Formulas over
Boolean and Linear Mathematical Propositions".
In Proc. 18th "Int. Conference of Automated Deduction, CADE'02."
LNAI ©
Springer Verlag.

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur
Kornilowicz, Roberto Sebastiani
"Integrating Boolean and Mathematical Solving:
Foundations, Basic Algorithms and Requirements".
In "Artificial Intelligence, Automated Reasoning, and Symbolic
Computation. Proc.
of Joint AISC 2002 and Calculemus 2002." Marseille, France, 2002.
LNAI N.2385 ©
Springer Verlag.
Other publications

Piotr Rudnicki and Andrzej Trybulec
Mathematical Knowledge Management in MIZAR,
in Proc. of the First International Workshop on Mathematical Knowledge Management: MKM'2001,
Bruno Buchberger and Olga Caprotti (Eds.)

Adam Grabowski
Robbins Algebras vs. Boolean Algebras,
in Proc. of the First International Workshop on Mathematical Knowledge Management: MKM'2001,
Bruno Buchberger and Olga Caprotti (Eds.)

Robert Milewski and Christoph Schwarzweller
Algebraic Requirements for the Construction of Polynomial Rings,
Mechanized Mathematics and Its Applications Vol. 2(1), August 2002.

Adam Naumowicz and Czeslaw Bylinski
Basic Elements of Computer Algebra in MIZAR,
Mechanized Mathematics and Its Applications Vol. 2(1), August 2002.
Development of the
Mizar Mathematical Library
 Christoph Schwarzweller,
The Binomial Theorem for Algebraic Structures,
Journal of Formalized Mathematics, Vol. 12.
 Jonathan Backer, Piotr Rudnicki and Christoph Schwarzweller,
Ring Ideals,
Journal of Formalized Mathematics, Vol. 12.
 Andrzej Trybulec,
Some Lemmas for the Jordan Curve Theorem,
Journal of Formalized Mathematics, Vol. 12.
 Artur Kornilowicz, Robert Milewski, Adam Naumowicz and Andrzej Trybulec,
Gauges and Cages, Part I,
Journal of Formalized Mathematics, Vol. 12.
 Robert Milewski, Andrzej Trybulec, Artur Kornilowicz and Adam Naumowicz,
Some Properties of Cells and Arcs,
Journal of Formalized Mathematics, Vol. 12.
 Adam Grabowski, Artur Kornilowicz and Andrzej Trybulec,
Some Properties of Cells and Gauges,
Journal of Formalized Mathematics, Vol. 12.
 Artur Kornilowicz and Robert Milewski,
Gauges and Cages. Part II,
Journal of Formalized Mathematics, Vol. 12.
 Andrzej Trybulec and Yatsuka Nakamura,
Again on the Order on a Special Polygon,
Journal of Formalized Mathematics, Vol. 12.
 Mariusz Giero and Roman Matuszewski,
Lower Tolerance. Preliminaries to Wroclaw Taxonomy,
Journal of Formalized Mathematics, Vol. 12.
 Mariusz Giero,
Hierarchies and Classifications of Sets,
Journal of Formalized Mathematics, Vol. 13.
 Andrzej Trybulec,
More on the Finite Sequences on the Plane,
Journal of Formalized Mathematics, Vol. 13.
 Ewa Gradzka,
The Algebra of Polynomials,
Journal of Formalized Mathematics, Vol. 13.
 Robert Milewski,
Upper and Lower Sequence of a Cage,
Journal of Formalized Mathematics, Vol. 13.
 Adam Naumowicz,
Some Remarks on Finite Sequences on Goboards,
Journal of Formalized Mathematics, Vol. 13.
 Robert Milewski,
Upper and Lower Sequence on the Cage. Part II,
Journal of Formalized Mathematics, Vol. 13.
 Andrzej Trybulec,
More on External Approximation of a Continuum,
Journal of Formalized Mathematics, Vol. 13.
 Adam Naumowicz and Robert Milewski,
Some Remarks on Clockwise Oriented Sequences on Goboards,
Journal of Formalized Mathematics, Vol. 14.
 Robert Milewski,
Upper and Lower Sequence on the Cage, Upper and Lower Arcs,
Journal of Formalized Mathematics, Vol. 14.
 Andrzej Trybulec,
Preparing the Internal Approximations of Simple Closed Curves,
Journal of Formalized Mathematics, Vol. 14.
 Mariusz Giero,
On the General Position of Special Polygons,
Journal of Formalized Mathematics, Vol. 14.
 Andrzej Trybulec,
Introducing Spans,
Journal of Formalized Mathematics, Vol. 14.
 Robert Milewski,
Properties of the Internal Approximation of Jordan's Curve,
Journal of Formalized Mathematics, Vol. 14.
 Robert Milewski,
Properties of the Upper and Lower Sequence on the Cage,
Journal of Formalized Mathematics, Vol. 14.
 Adam Grabowski,
On the Decompositions of Intervals and Simple Closed Curves,
Journal of Formalized Mathematics, Vol. 14.
 Andrzej Trybulec,
On the Minimal Distance Between Set in Euclidean Space,
Journal of Formalized Mathematics, Vol. 14.
 Yatsuka Nakamura and Andrzej Trybulec,
Sequences of Metric Spaces and
an Abstract Intermediate Value Theorem,
Journal of Formalized Mathematics, Vol. 14.
 Andrzej Trybulec and Yatsuka Nakamura,
On the Decomposition of a Simple Closed Curve into Two Arcs,
Journal of Formalized Mathematics, Vol. 14.
 Artur Kornilowicz,
The Ordering of Points on a Curve, Part III,
Journal of Formalized Mathematics, Vol. 14.
 Artur Kornilowicz,
The Ordering of Points on a Curve, Part IV,
Journal of Formalized Mathematics, Vol. 14.
 Josef Urban,
Order Sorted Algebras,
Journal of Formalized Mathematics, Vol. 14.
 Josef Urban,
Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras,
Journal of Formalized Mathematics, Vol. 14.
 Josef Urban,
Homomorphisms of Order Sorted Algebras,
Journal of Formalized Mathematics, Vol. 14.
 Josef Urban,
Order Sorted Quotient Algebra,
Journal of Formalized Mathematics, Vol. 14.
 Josef Urban,
Free Order Sorted Universal Algebra,
Journal of Formalized Mathematics, Vol. 14.