nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

Mizar: State-of-the-art and Beyond

verfasst von : Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pa̧k, Josef Urban

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Mizar is one of the pioneering systems for mathematics formalization, which still has an active user community. The project has been in constant development since 1973, when Andrzej Trybulec designed the fundamentals of a language capable of rigorously encoding mathematical knowledge in a computerized environment which guarantees its full logical correctness. Since then, the system with its feature-rich language devised to approximate mathematics writing has influenced other formalization projects and has given rise to a number of Mizar modes implemented on top of other systems. However, the information about the system as a whole is not readily available to developers of other systems. Various papers describing Mizar features have been rather incremental and focused only on particular newly implemented Mizar aspects. The objective of the current paper is to give a survey of the most important Mizar features that distinguish it from other popular proof checkers. We also go a step further and describe most important current trends and lines of development that go beyond the state-of-the-art system.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Performance Evaluation and Optimization of Math-Similarity Search

Nächstes Kapitel Growing the Digital Repository of Mathematical Formulae with Generic LaTex Sources

http://www.cl.cam.ac.uk/~jrh13/hol-light/.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/.

http://coq.inria.fr.

http://us.metamath.org.

http://www.lemma-one.com/ProofPower/index/.

http://www.cs.utexas.edu/users/moore/acl2/.

http://pvs.csl.sri.com.

http://www.nuprl.org.

Generated with MML Query, http://mmlquery.mizar.org.

The description of the Mizar grammar can be found at http://mizar.uwb.edu.pl/language/.

http://github.com/JUrban/xsl4mizar.

http://mizar.cs.ualberta.ca/~mptp/MizAR.html.

http://fm.uwb.edu.pl/proof-read/.

Alama, J.: Mizar-items: exploring fine-grained dependencies in the Mizar mathematical library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM/Calculemus 2011. LNCS, vol. 6824, pp. 276–277. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1_19 CrossRef

Alama, J.: Escape to Mizar from ATPs. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, 30 June–1 July 2012. EPiC Series, vol. 21, pp. 3–11. EasyChair (2012). http://www.easychair.org/publications/?page=1559779348

Alama, J.: Eliciting implicit assumptions of Mizar proofs by property omission. J. Autom. Reasoning 50(2), 123–133 (2013). http://dx.doi.org/ 10.1007/s10817-012-9264-3 MathSciNetCrossRefMATH

Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: issues and solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM/Calculemus 2011. LNCS, vol. 6824, pp. 133–148. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1 CrossRef

Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar mathematical library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011/Calculemus 2011. LNCS, vol. 6824, pp. 149–163. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-22673-1_11 CrossRef

Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 1–16. Springer, Heidelberg (2012). http://dx.doi.org/ 10.1007/978-3-642-31374-5_1 CrossRef

Anonymous: the QED manifesto. Bundy, A. (ed.) CADE 1994. LNCS, vol. 814. Springer, Heidelberg (1994)

Strotmann, A.: The categorial type of OpenMath objects. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 378–392. Springer, Heidelberg (2004) CrossRef

Bancerek, G.: Automatic translation in formalized mathematics. Mech. Math. Appl. 5(2), 19–31 (2006)

10.

Bancerek, G.: Information retrieval and rendering with MML query. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 266–279. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11812289_21 CrossRef

11.

Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in Mizar: formalizing recent mathematics. J. Autom. Reason. 29(3–4), 189–224 (2002)MathSciNetCrossRefMATH

12.

Bancerek, G., Rudnicki, P.: Information retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 119–132. Springer, Heidelberg (2003)CrossRef

13.

Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 44–57. Springer, Heidelberg (2004) CrossRef

14.

Bylinski, C., Alama, J.: New developments in parsing Mizar. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 427–431. Springer, Heidelberg (2012) CrossRef

15.

Cairns, P.: Informalising formal mathematics: searching the Mizar library with latent semantics. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 58–72. Springer, Heidelberg (2004) CrossRef

16.

Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69–84. Springer, Heidelberg (2008). http://dx.doi.org/10.1007/978-3-540-68103-8_5 CrossRef

17.

Botana, F.: A symbolic companion for interactive geometric systems. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 285–286. Springer, Heidelberg (2011) CrossRef

18.

Futa, Y., Okazaki, H., Shidama, Y.: Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. J. Autom. Reason. 50(2), 161–172 (2013). http://dx.doi.org/10.1007/s10817-012-9265-2 MathSciNetCrossRefMATH

19.

Gow, J., Cairns, P.: Closing the gap between formal and digital libraries of mathematics. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, University of Białystok, vol. 10(23), pp. 249–263 (2007). http://mizar.org/trybulec65/

20.

Grabowski, A.: Efficient rough set theory merging. Fundamenta Informaticae 135(4), 371–385 (2014). http://dx.doi.org/10.3233/FI-2014-1129 MathSciNetMATH

21.

Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010)MathSciNetMATH

22.

Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 49–64. Springer, Heidelberg (2006). http://dx.doi.org/10.1007/11618027_4 CrossRef

23.

Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 235–249. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-73086-6_20 CrossRef

24.

Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of Federated Conference on Computer Science and Information Systems - FedCSIS 2012, Wroclaw, Poland, 9–12 September 2012, pp. 63–68 (2012)

25.

Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996). http://dl.acm.org/citation.cfm?id=646523.694700

26.

Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191–202 (2013). http://dx.doi.org/10.1007/s10817-012-9271-4 MathSciNetCrossRefMATH

27.

Jaśkowski, S.: On the Rules of Suppositions in Formal Logic. Studia Logica, Nakładem Seminarjum Filozoficznego Wydziału Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego (1934). http://books.google.pl/books?id=6w0vRAAACAAJ

28.

Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40 (2013). CoRR abs/1310.2805

29.

Kaliszyk, C., Urban, J., Vyskočil, J.: Machine learner for automated reasoning 0.4 and 0.5 (2014). Accepted to PAAR 2014, CoRR abs/1402.2359

30.

Korniłowicz, A.: Jordan curve theorem. Formaliz. Math. 13(4), 481–491 (2005)

31.

Korniłowicz, A.: On rewriting rules in Mizar. J. Autom. Reason. 50(2), 203–210 (2013). http://dx.doi.org/10.1007/s10817-012-9261-6 MathSciNetCrossRefMATH

32.

Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. In: Mechanized Mathematicsand Its Applications, Special Issue on 30 Years of Mizar, vol. 4, no. 1, pp. 3–24 (2005)

33.

Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. J. Appl. Logic 4(4), 396–413 (2006). http://www.sciencedirect.com/ science/article/pii/S1570868305000686 MathSciNetCrossRefMATH

34.

Naumowicz, A.: Enhanced processing of adjectives in Mizar. In: Grabowski, A., Naumowicz, A. (eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric, University of Białystok, vol. 18, no. 31, pp. 89–101 (2009)

35.

Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010). http://dx.doi.org/10.1080/00207160701864459 CrossRefMATH

36.

Naumowicz, A.: SAT-enhanced Mizar proof checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 449–452. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/ 978-3-319-08434-3_37 CrossRef

37.

Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004). http://dx.doi.org/ 10.1007/978-3-540-27818-4_21 CrossRef

38.

Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009). http://dx.doi.org/10.1007/978-3-642-03359-9_5 CrossRef

39.

Pa̧k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013). http://dx.doi.org/10.1007/s10817-012-9267-0 MathSciNetCrossRef

40.

Pa̧k, K.: Improving legibility of natural deduction proofs is not trivial. Logic. Methods Comput. Sci. 10(3), 1–30 (2014). http://dx.doi.org/10.2168/ LMCS-10(3:23)2014 MathSciNet

41.

Rudnicki, P., Trybulec, A.: On the integrity of a repository of formal mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 162–174. Springer, Heidelberg (2003) CrossRef

42.

Syme, D.: DECLARE: a prototype declarative proof system for higher order logic. Technical report, University of Cambridge (1997)

43.

Trybulec, A., Korniłowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reason. 50(2), 119–121 (2013). http://dx.doi.org/ 10.1007/s10817-012-9268-z CrossRef

44.

Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP semantic presentation and verification tools. Stud. Logic Gramm. Rhetor. 18(31), 121–136 (2009)

45.

Urban, J.: MPTP - motivation, implementation, first experiments. J. Autom. Reason. 33(3–4), 319–339 (2004)MathSciNetCrossRefMATH

46.

Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006) CrossRef

47.

Urban, J.: MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Logic 4(4), 414–427 (2006). http://dx.doi.org/ 10.1016/j.jal.2005.10.004 MathSciNetCrossRefMATH

48.

Urban, J.: MoMM – fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109–130 (2006). http://ktiml.mff.cuni.cz/urban/MoMM/momm.ps CrossRef

49.

Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1–2), 21–43 (2006). http://dx.doi.org/10.1007/s10817-006-9032-3 MATH

50.

Urban, J.: BliStr: The Blind Strategymaker (2014). Accepted to PAAR 2014, CoRR abs/1301.2683

51.

Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: motivation, considerations, and initial prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol. 6167, pp. 455–469. Springer, Heidelberg (2010) CrossRef

52.

Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50(2), 229–241 (2013). http://dx.doi.org/10.1007/ s10817-012-9269-y MathSciNetCrossRefMATH

53.

Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Math. Comput. Sci. 2(2), 231–251 (2008). http://dx.doi.org/10.1007/s11786-008-0053-7 MathSciNetCrossRefMATH

54.

Urban, J., Sutcliffe, G., Pudlák, P., Vyskočil, J.: MaLARea SG1 - machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008) CrossRef

55.

Urban, J., Vyskočil, J., Štěpánek, P.: MaLeCoP machine learning connection prover. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 263–277. Springer, Heidelberg (2011) CrossRef

56.

Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2003). http://dx.doi.org/10.1023/A:1021935419355 MathSciNetMATH

57.

Wiedijk, F.: Mizar light for HOL light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 378–394. Springer, Heidelberg (2001) CrossRef

58.

Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 378–393. Springer, Heidelberg (2004) CrossRef

59.

Gamboa, R.: ACL2. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol. 3600, pp. 55–66. Springer, Heidelberg (2006) CrossRef

60.

Wiedijk, F.: Formal proof–getting started. Not. Am. Math. Soc. 55(11), 1408–1414 (2008)MathSciNetMATH

61.

Wiedijk, F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Logic. Methods Comput. Sci. 8(1:30), 1–26 (2012)MathSciNetMATH

Titel: Mizar: State-of-the-art and Beyond
verfasst von: Grzegorz Bancerek
Czesław Byliński
Adam Grabowski
Artur Korniłowicz
Roman Matuszewski
Adam Naumowicz
Karol Pa̧k
Josef Urban
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-319-20614-1

Electronic ISBN: 978-3-319-20615-8

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-319-20615-8_17

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"