Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

On Semilattice Structure of Mizar Types


Grzegorz Bancerek
Bialystok Technical University

Summary.

The aim of this paper is to develop a formal theory of Mizar types. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier and formalization of the ideas from [9].

MML Identifier: ABCMIZ_0

The terminology and notation used in this paper have been introduced in the following articles [18] [13] [22] [24] [21] [23] [3] [19] [1] [11] [12] [16] [10] [14] [15] [4] [2] [20] [5] [6] [7] [8] [17]

Contents (PDF format)

  1. Semilattice of Widening
  2. Adjectives
  3. Applicability of Adjectives
  4. Subject Function
  5. Reduction of Adjectives
  6. Radix Types

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[5] Grzegorz Bancerek. Complete lattices. Journal of Formalized Mathematics, 4, 1992.
[6] Grzegorz Bancerek. Reduction relations. Journal of Formalized Mathematics, 7, 1995.
[7] Grzegorz Bancerek. Bounds in posets and relational substructures. Journal of Formalized Mathematics, 8, 1996.
[8] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.
[9] Grzegorz Bancerek. On the structure of Mizar types. In Herman Geuvers and Fairouz Kamareddine, editors, \em Electronic Notes in Theoretical Computer Science, volume 85. Elsevier, 2003.
[10] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[11] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[12] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[13] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[14] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[15] Czeslaw Bylinski. Some properties of restrictions of finite sequences. Journal of Formalized Mathematics, 7, 1995.
[16] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[17] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Journal of Formalized Mathematics, 8, 1996.
[18] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[19] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.
[20] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[21] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[22] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[23] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[24] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.

Received August 8, 2003

[ Download a postscript version, MML identifier index, Mizar home page]