Calculemus
System for Integrated Computation and Deduction funded under the 5th Framework Programme of the European Commission
Contract Reference HPRN-CT-2000-00102
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:

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:

The research within Calculemus tasks stimulated the following evolution of Mizar system:

Networking

Joint publications

  1. 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.
  2. 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.
  3. 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

  1. 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.)
  2. 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.)
  3. Robert Milewski and Christoph Schwarzweller
    Algebraic Requirements for the Construction of Polynomial Rings,
    Mechanized Mathematics and Its Applications Vol. 2(1), August 2002.
  4. 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

  1. Christoph Schwarzweller, The Binomial Theorem for Algebraic Structures, Journal of Formalized Mathematics, Vol. 12.
  2. Jonathan Backer, Piotr Rudnicki and Christoph Schwarzweller, Ring Ideals, Journal of Formalized Mathematics, Vol. 12.
  3. Andrzej Trybulec, Some Lemmas for the Jordan Curve Theorem, Journal of Formalized Mathematics, Vol. 12.
  4. Artur Kornilowicz, Robert Milewski, Adam Naumowicz and Andrzej Trybulec, Gauges and Cages, Part I, Journal of Formalized Mathematics, Vol. 12.
  5. Robert Milewski, Andrzej Trybulec, Artur Kornilowicz and Adam Naumowicz, Some Properties of Cells and Arcs, Journal of Formalized Mathematics, Vol. 12.
  6. Adam Grabowski, Artur Kornilowicz and Andrzej Trybulec, Some Properties of Cells and Gauges, Journal of Formalized Mathematics, Vol. 12.
  7. Artur Kornilowicz and Robert Milewski, Gauges and Cages. Part II, Journal of Formalized Mathematics, Vol. 12.
  8. Andrzej Trybulec and Yatsuka Nakamura, Again on the Order on a Special Polygon, Journal of Formalized Mathematics, Vol. 12.
  9. Mariusz Giero and Roman Matuszewski, Lower Tolerance. Preliminaries to Wroclaw Taxonomy, Journal of Formalized Mathematics, Vol. 12.
  10. Mariusz Giero, Hierarchies and Classifications of Sets, Journal of Formalized Mathematics, Vol. 13.
  11. Andrzej Trybulec, More on the Finite Sequences on the Plane, Journal of Formalized Mathematics, Vol. 13.
  12. Ewa Gradzka, The Algebra of Polynomials, Journal of Formalized Mathematics, Vol. 13.
  13. Robert Milewski, Upper and Lower Sequence of a Cage, Journal of Formalized Mathematics, Vol. 13.
  14. Adam Naumowicz, Some Remarks on Finite Sequences on Go-boards, Journal of Formalized Mathematics, Vol. 13.
  15. Robert Milewski, Upper and Lower Sequence on the Cage. Part II, Journal of Formalized Mathematics, Vol. 13.
  16. Andrzej Trybulec, More on External Approximation of a Continuum, Journal of Formalized Mathematics, Vol. 13.
  17. Adam Naumowicz and Robert Milewski, Some Remarks on Clockwise Oriented Sequences on Go-boards, Journal of Formalized Mathematics, Vol. 14.
  18. Robert Milewski, Upper and Lower Sequence on the Cage, Upper and Lower Arcs, Journal of Formalized Mathematics, Vol. 14.
  19. Andrzej Trybulec, Preparing the Internal Approximations of Simple Closed Curves, Journal of Formalized Mathematics, Vol. 14.
  20. Mariusz Giero, On the General Position of Special Polygons, Journal of Formalized Mathematics, Vol. 14.
  21. Andrzej Trybulec, Introducing Spans, Journal of Formalized Mathematics, Vol. 14.
  22. Robert Milewski, Properties of the Internal Approximation of Jordan's Curve, Journal of Formalized Mathematics, Vol. 14.
  23. Robert Milewski, Properties of the Upper and Lower Sequence on the Cage, Journal of Formalized Mathematics, Vol. 14.
  24. Adam Grabowski, On the Decompositions of Intervals and Simple Closed Curves, Journal of Formalized Mathematics, Vol. 14.
  25. Andrzej Trybulec, On the Minimal Distance Between Set in Euclidean Space, Journal of Formalized Mathematics, Vol. 14.
  26. Yatsuka Nakamura and Andrzej Trybulec, Sequences of Metric Spaces and an Abstract Intermediate Value Theorem, Journal of Formalized Mathematics, Vol. 14.
  27. Andrzej Trybulec and Yatsuka Nakamura, On the Decomposition of a Simple Closed Curve into Two Arcs, Journal of Formalized Mathematics, Vol. 14.
  28. Artur Kornilowicz, The Ordering of Points on a Curve, Part III, Journal of Formalized Mathematics, Vol. 14.
  29. Artur Kornilowicz, The Ordering of Points on a Curve, Part IV, Journal of Formalized Mathematics, Vol. 14.
  30. Josef Urban, Order Sorted Algebras, Journal of Formalized Mathematics, Vol. 14.
  31. Josef Urban, Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras, Journal of Formalized Mathematics, Vol. 14.
  32. Josef Urban, Homomorphisms of Order Sorted Algebras, Journal of Formalized Mathematics, Vol. 14.
  33. Josef Urban, Order Sorted Quotient Algebra, Journal of Formalized Mathematics, Vol. 14.
  34. Josef Urban, Free Order Sorted Universal Algebra, Journal of Formalized Mathematics, Vol. 14.