Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

A Compendium of Continuous Lattices in MIZAR

A Compendium of Continuous Lattices in MIZAR This paper reports on the MIZAR formalization of the theory of continuous lattices as presented in Gierz et al.: A Compendium of Continuous Lattices, 1980. 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 the Gierz et al. compendium has (i) prompted many improvements of the MIZAR proof checking system, (ii) caused numerous revisions of the the MIZAR data base, and (iii) contributed to the “to do” list of further changes to the MIZAR system. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

A Compendium of Continuous Lattices in MIZAR

Loading next page...
 
/lp/springer-journals/a-compendium-of-continuous-lattices-in-mizar-0KWgZphRfl

References (76)

Publisher
Springer Journals
Copyright
Copyright © 2002 by Kluwer Academic Publishers
Subject
Philosophy; Logic; Symbolic and Algebraic Manipulation; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1023/A:1021966832558
Publisher site
See Article on Publisher Site

Abstract

This paper reports on the MIZAR formalization of the theory of continuous lattices as presented in Gierz et al.: A Compendium of Continuous Lattices, 1980. 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 the Gierz et al. compendium has (i) prompted many improvements of the MIZAR proof checking system, (ii) caused numerous revisions of the the MIZAR data base, and (iii) contributed to the “to do” list of further changes to the MIZAR system.

Journal

Journal of Automated ReasoningSpringer Journals

Published: Sep 30, 2004

There are no references for this article.