A Compendium of Continuous Lattices in MIZAR
Tóm tắt
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.
Tài liệu tham khảo
Bancerek, G.: Tarski's classes and ranks, Formalized Mathematics 1(3) (1990), 563–567. MML: CLASSES1.
Bancerek, G.: König's theorem, Formalized Mathematics 1(3) (1990), 589–593. MML: CARD_3.
Bancerek, G.: Complete lattices, Formalized Mathematics 2(5) (1991), 719–725. MML: LATTICE3.
Bancerek, G.: Bounds in posets and relational substructures, Formalized Mathematics 6(1) (1997), 81–91. MML: YELLOW_0.
Bancerek, G.: Directed sets, nets, ideals, filters, and maps, Formalized Mathematics 6(1) (1997), 93–107. MML: WAYBEL_0.
Bancerek, G.: The “way-below” relation, FormalizedMathematics 6(1) (1997), 169–176. MML: WAYBEL_3.
Bancerek, G.: Duality in relation structures, Formalized Mathematics 6(2) (1997), 227–232. MML: YELLOW_7.
Bancerek, G.: Prime ideals and filters, Formalized Mathematics 6(2) (1997), 241–247. MML
Bancerek, G.: Bases and refinements of topologies, Formalized Mathematics 7(1) (1998), 35–43. MML: YELLOW_9.
Bancerek, G.: The Lawson topology, Formalized Mathematics 7(2) (1998), 163–168. MML: WAYBEL19.
Bancerek, G.: Lawson topology in continuous lattices, Formalized Mathematics 7(2) (1998), 177–184. MML: WAYBEL21.
Bancerek, G.: Development of the theory of continuous lattices in MIZAR, in M. Kerber and M. Kohlhase (eds), Symbolic Computation and Automated Reasoning, A. K. Peters, 2001.
Bancerek, G.: Continuous lattices of maps between T0 spaces, Formalized Mathematics 9(1) (2001), 111–117. MML: WAYBEL26.
Bancerek, G.: Categorial background for duality theory, Formalized Mathematics 9(4) (2001), 755–765. MML: YELLOW21.
Bancerek, G.: Duality based on the Galois connection. Part I, Formalized Mathematics 9(4) (2001), 767–778. MML: WAYBEL34.
Bancerek, G., Endou, N. and Shidama, Y.: Lim-inf convergence and its compactness, Mechanized Mathematics and Its Applications 2(1) (2002), 29–35.
Byli´nski, C.: Some basic properties of sets, Formalized Mathematics 1(1) (1990), 47–53. MML: ZFMISC_1.
Byli´nski, C.: Introduction to categories and functors, Formalized Mathematics 1(2) (1990), 409–420. MML: CAT_1.
Byli´nski, C.: Category ens, Formalized Mathematics 2(4) (1991), 527–533. MML: ENS_1.
Byli´nski, C.: Galois connections, Formalized Mathematics 6(1) (1997), 131–143. MML: WAYBEL_1.
Byli´nski, C. and Rudnicki, P.: The Scott topology. Part II, Formalized Mathematics 6(3) (1997), 441–446. MML: WAYBEL14.
Fleuriot, J. and Paulson, L. C.: A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia, in C. Kirchner and H. Kirchner (eds), 15th International Conf. on Automated Deduction: CADE-15, LNAI 1421, Springer, 1998, pp. 3–16.
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. W. and Scott, D. S.: A Compendium of Continuous Lattices, Springer-Verlag, Berlin, 1980.
Grabowski, A. and Milewski, R.: Boolean posets, posets under inclusion and products of relational structures, Formalized Mathematics 6(1) (1997), 117–121. MML: YELLOW_1.
Gryko, J.: Injective spaces, Formalized Mathematics 7(1) (1998), 57–62. MML: WAYBEL18.
Ja´skowski, S.: On the Rules of Supposition in Formal Logic, Studia Logica,Warsaw University, 1934. Reprinted in S. McCall, Polish Logic in 1920–1939, Clarendon Press, Oxford.
Johnstone, P. T.: Stone Spaces, Cambridge University Press, Cambridge, 1982.
van Benthem Jutting, L. S.: Checking Landau's “Grundlagen” in the Automath system, Ph.D. thesis, The Eindhoven, 1977.
Kelley, J. L.: General Topology, Van Nostrand, New York, 1955.
Korniłowicz, A.: Cartesian products of relations and relational structures, Formalized Mathematics 6(1) (1997), 145–152. MML: YELLOW_3.
Korniłowicz, A.: On the topological properties of meet-continuous lattices, Formalized Mathematics 6(2) (1997), 269–277. MML: WAYBEL_9.
Landau, E. G. H.: Grundlagen der Analysis, Akademische Verlag, Leipzig, 1930.
Library Committee of the Association of Mizar Users. Preliminaries to Structures, JFM, Addenda. MML: STRUCT_0.
Library Committee of the Association of Mizar Users. Preliminaries to Arithmetic, JFM, Addenda. MML: ARYTM.
MIZAR Manuals. http://mizar.org/project/bibliography.html.
Madras, B.: Product of family of universal algebras, Formalized Mathematics 4(1) (1993), 103–108. MML: PRALG_1.
Milewski, R.: Algebraic lattices, Formalized Mathematics 6(2) (1997), 249–254. MML: WAYBEL_8.
Nederpelt, R. P., Geuvers, J. H. and de Vrijer, R. C.: Selected Papers on Automath, North-Holland, Amsterdam, 1994.
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook, Formal Aspects of Computing 10 (1998), 171–186.
Padlewska, B. and Darmochwał, A.: Topological spaces and continuous functions, Formalized Mathematics 1(1) (1990), 223–230. MML: PRE_TOPC.
Paulson, L. C. and Grabczewski, K.: Mechanizing set theory: Cardinal arithmetic and the axiom of choice, J. Automated Reasoning 17 (1996), 291–323.
Rasiowa, H. and Sikorski, R.: The Mathematics of Metamathematics, PWN, Warszawa, 1968.
Rudnicki, P.: Kernel projections and quotient lattices, Formalized Mathematics 7(2) (1998), 169–175. MML: WAYBEL20.
Rudnicki, P., Schwarzweller, Ch. and Trybulec, A.: Commutative algebra in the Mizar system, J. Symbolic Comput. 32 (2001), 143–169.
Rudnicki, P. and Trybulec, A.: On equivalents of well-foundedness, J. Automated Reasoning 23(3–4) (1999), 197–234.
Rudnicki, P. and Trybulec, A.: Mathematical knowledge management in MIZAR, 1st Int.Workshop on MKM, Sept. 24–26, 2001. http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001.
Shibakov, A Yu. and Trybulec, A.: The Cantor set, Formalized Mathematics 5(2) (1996), 233–236. MML: CANTOR_1.
Trybulec, A.: Tarski Grothendieck set theory, Formalized Mathematics 1(1) (1990), 9–11. MML: TARSKI.
Trybulec, A.: Built-in concepts, Formalized Mathematics 1(1) (1990), 13–15. MML: AXIOMS.
Trybulec, A.: Categories without uniqueness of cod and dom, Formalized Mathematics 5(2) (1996), 259–267. MML: ALTCAT_1.
Trybulec, A.: Functors for alternative categories, Formalized Mathematics 5(4) (1996), 595–608. MML: FUNCTOR0.
Trybulec, A.: Moore–Smith convergence, Formalized Mathematics 6(2) (1997), 213–225.
Trybulec A.: Scott topology, Formalized Mathematics 6(2) (1997), 311–319. MML: WAYBEL11.
Trybulec, W. A.: Partially ordered sets, Formalized Mathematics 1(2) (1990), 313–319. MML: ORDERS_1.
Trybulec, Z. and Świ¸eczkowska, H.: Boolean properties of sets, Formalized Mathematics 1(1) (1990), 17–23. MML: BOOLE.
Wiedijk, F.: Mizar: An impression. http://www.cs.kun.nl/~freek/notes.
Wiedijk, F.: Estimating the cost of a standard library for a mathematical proof checker. http: //www.cs.kun.nl/~freek/notes.
Wiedijk, F.: The de Bruijn factor. http://www.cs.kun.nl/~freek/notes.
Woronowicz, E. and Zalewska, A.: Properties of binary relations, Formalized Mathematics 1(1) (1990), 85–89. MML: RELAT_2.
Żukowski, S.: Introduction to lattice theory, Formalized Mathematics 1(1) (1990), 215–222. MML: LATTICES.