×

A compendium of continuous lattices in MIZAR. (English) Zbl 1064.68082

Summary: This paper reports on the MIZAR formalization of the theory of continuous lattices as presented by G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott [(*) A compendium of continuous lattices. Berlin: Springer (1980; Zbl 0452.06001)]. By a MIZAR formalization we mean a formulation of theorems, definitions, and proofs written in the MIZAR language whose correctness is verified by the MIZAR processor. This effort was originally motivated by the question of whether or not the MIZAR system was sufficiently developed for the task of expressing advanced mathematics. The current state of the formalization – 57 MIZAR articles written by 16 authors – indicates that in principle the MIZAR system has successfully met the challenge. To our knowledge it is the most sizable effort aimed at mechanically checking some substantial and relatively recent field of advanced mathematics. However, it does not mean that doing mathematics in MIZAR is as simple as doing mathematics traditionally (if doing mathematics is simple at all). The work of formalizing the material of (*) has (i) prompted many improvements of the MIZAR proof checking system, (ii) caused numerous revisions of the MIZAR data base, and (iii) contributed to the “to do” list of further changes to the MIZAR system.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
06B35 Continuous lattices and posets, applications

Citations:

Zbl 0452.06001

Software:

Mizar; Automath
PDFBibTeX XMLCite
Full Text: DOI