Exploring MiZAR library with MML Query

• Autorzy: Bancerek G.

Warianty tytułu

PL

Eksploracja biblioteki mizara z użyciem MML Query

• Języki publikacji: EN

Abstrakty

EN

MiZAR, a proof-checking system, is used to build the MiZAR Mathematical Li-brary (MML). MML Query is a semantics-based tool for managing the mathematical knowl-edge in MiZAR including searching, browsing and presentation of the evolving MML content. The tool is becoming widely used as an aid for MiZAR authors and plays an essential role in the ongoing reorganization of MML. In the paper, we briefly present MiZAR system including language, tools for logical verifi-cation and publishing, foundations of MML, its content and maintenance, and the problems raising when using the MML (information retrieval and rendering). We also present the pos-sibilities offered by MML Query to solve these problems.

PL

MlZAR(komputerowy system weryfikacji dowodów) jest używany do budowania MiZAR Mathematical Library (MML). MML Query jest narzędziem opartym o semantykę tekstu mizarowego służącym do zarządzania wiedzą w systemie MiZAR włączając w to wyszukiwanie, przeglądanie i prezentację ewolującej zawartości MML. Narzędzie to stało się szeroko używane jako pomoc dla autorów mizarowych oraz odgrywa istotną rolę w nieustających reorganizacjach MML. W artykule zaprezentowane są elementy systemu MiZAR i MML Query jak język, narzędzia logicznej weryfikacji i automatycznej publikacji, podstawy biblioteki MML, jej zawartość i konserwacja oraz problemy pojawiające się przy używaniu MML (odzyskiwanie informacji orazjej przedstawianie). Ponadto, są przedstawione możliwości MMLQuery w rozwiązywaniu tych problemów.

Słowa kluczowe

EN

MIZAR; sematic searching; repositories of formalized mathematics

PL

MIZAR; wyszukiwanie semantyczne; repozytoria sformalizowanej matematyki

• Wydawca: Oficyna Wydawnicza Politechniki Białostockiej
• Czasopismo: Zeszyty Naukowe Politechniki Białostockiej. Informatyka
• Rocznik: 2007
• Tom: Z. 2
• Strony: 5--18
• Opis fizyczny: Bibliogr. 25 poz.

Twórcy

autor

Bancerek G.

• Białystok Technical University, Faculty of Computer Science, Białystok

Bibliografia

• cytowania@=25
• [1] Bancerek, G.: Automatic translation in Formalized Mathematics, Mechanized Mathematics and Its Applications, 5(2): 19-31, 2006, MIZAR Japan.
• [2] Bancerek, G.: Cardinal Arithmetics, Formalized Mathematics, l(3):543-547, 1990.
• [3] Bancerek, G.: Development of the theory of continuous lattices in MlZAR, in M. Kerber and M. Kohlhase (eds), Symbolic Computation and Automated Reasoning, 65-80, A. K.Peters, 2001.
• [4] Bancerek, G.: Information retrieval and rendering with MML Query, in J.M. Borwein, W.M. Farmer (eds), Proceedings of MKM 2006, Wokingham, UK, LNAI, 4108: 266-279, 2006.
• [5] Bancerek, G.: On Constructing Topological Spaces and Sorgenfrey Linę, Formalized Mathematics, 13(1): 171-179, 2005.
• [6] Bancerek, G.: The Reflection Theorem, Formalized Mathematics, 1(5):963-972, 1990.
• [7] Bancerek, G.: On the structure of Mizar types. Electronic Notes in Theoretical Computer Science, Vol. 85 (7), Elsevier, 2003.
• [8] Bancerek, G., Endou, N., Shidama, Y.: Lim-inf Convergence and its Compact-ness. Mechanized Mathematics and Its Applications, 2(1): 29-35, 2002.
• [9] Bancerek, G., Rudnicki, R: A Compendium of Continuous Lattices in MiZAR, Journal ofAutomated Reasoning, 29(3-4): 189-224, 2002.
• [10] Bancerek, G., Rudnicki, R: Information retrieval in MML, in A. Asperti, B. Buchberger, J. H. Davenport (eds), Proceedings of MKM 2003, Bertinoro, LNCS, 2594: 119-131,2003.
• [11] Bancerek, G., Urban, J.: Integrated Semantic Browsing of the Mizar Mathe¬matical Library for Authoring Mizar Articles, in Asperti, A., Bancerek, G., Trybulec, A. (eds), Proceedings of MKM 2004, Białowieża, LNCS, 3119: 44-57, 2004.
• [12] Braselmann, R, Koepke, R: GódeFs Completeness Theorem, Formalized Mathematics, 13(l):49-53, 2005.
• [13] Dahn, I.: Management of Informal Mathematics Knowledge-Lessons Learned from the Trial-Solution Project, in Bai, E, Wegner, B., Electronic Information and Communication in Mathematics, LNCS 2730:29-43, 2003.
• [14] Gierz, G., K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, D. S. Scott. A Compendium of Continuous Lattices, Springer-Verlag, Berlin, 1980.
• [15] M. Kohlhase (joint work with Bancerek, G.). Towards MIZAR Mathematical Library in OMDOC format. Electronic Proceedings of the Workshop Math¬ematics on the Semantic Web, Eindhoven, 2003, http://www.win.tue.nl/ dw/monet/proceedings/kohlhase-mizarinomdoc.ps
• [16] Korniłowicz, A.: Jordan Curve Theorem, Formalized Mathematics, 13(4):481-491,2005.
• [17] R. Matuszewski, Rudnicki, R: MiZAR: the first 30 years. Mechanized Mathe¬matics and Its Applications, 4(l):3-24, 2005.
• [18] R.Milewski. Fundamental Theorem of Algebra, Formalized Mathematics, 9(3):461-470,2001.
• [19] Rudnicki, R, Ch. Schwarzweller, A. Trybulec. Commutative Algebra in the Mizar System. Journal ofSymbolic Computation, 32:143-169, 2001.
• [20] Rudnicki, R, A. Trybulec. On equivalents of well-foundedness. Journal of Automated Reasoning, 23(3-4): 197-234, 1999.
• [21] J. Urban. MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic, 2005, doi: 10.1016/ j.jal.2005.10.004Grzegorz Bancerek
• [22] J. Urban. MoMM - fast interreduction and retrieval in large libraries of formal-ized mathematics. International Journal on Artificial Intelligence Tools, 15(1):109-130,2006.
• [23] J. Urban. XML-izing Mizar: making semantic processing and presentation ofMML easy. in M. Kohlhase (ed), Proceedings of MKM 2005, Bremen, LNCS,3863: 346-360, 2006.
• [24] J. Urban, Bancerek, G.: Presenting and Explaining Mizar. in S. Autexier andC. Benzmuller (eds), Proceedings of UITP 2006, IJCAR'06 Workshop, Seattle,97-108,2006.
• [25] Wiedijk, F.: Mizar: An Impression. http://www.cs.kun.nl/~freek/notes.Partially supported by Białystok Technical University grant W/WI/1/06