Abstract
The Mizar Verifier uses definitional expansions for controlling proof structures. In this paper we propose another use of definitional expansions—enriching verified inferences by expansions of definitions of formulae included in the inferences and increasing the number of premises accessible by Checker. This introduces more knowledge to the reasoning, which helps to draw more conclusions. Some statistics about influence of such expansions on the Mizar Mathematical Library are presented.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H. et al. (eds.) Proceedings of Calculemus/MKM 2011, LNCS, vol. 6824, pp. 149–163. Springer-Verlag, Berlin, Heidelberg. doi: 10.1007/978-3-642-22673-1_11 (2011)
Bancerek, G.: Information retrieval and rendering with MML query. In: Borwein, J. et al. (eds.) Mathematical Knowledge Management, LNCS, vol. 4108, pp. 266–279. Springer Berlin Heidelberg. doi: 10.1007/11812289_21 (2006)
Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar Mathematical Library for authoring Mizar articles. In: Asperti, A. et al. (eds.) MKM 2004, Bialowieza, Poland, September 2004, Proceedings, LNCS, vol. 3119, pp. 44–57. Springer. doi: 10.1007/978-3-540-27818-4_4 (2004)
Barker-Plummer, D.: Gazing: An approach to the problem of definition and lemma use. J. Autom. Reasoning 8(3), 311–344 (1992)
Bishop, M., Andrews, P.B.: Selectively instantiating definitions. In: CADE-15, Lindau, Germany, July, 1998, Proceedings, LNCS, vol. 1421, pp. 365–380. Springer (1998)
Bledsoe, W.W.: The UT interactive prover. Memo ATP-17B, Mathematics Department. University of Texas (1983)
Bylinski, C., Alama, J.: New developments in parsing Mizar. In: Jeuring, J. et al. (eds.) Intelligent Computer Mathematics 11th International Conference LNAI vol. 7362, pp. 427–431 Springer-Verlag Berlin Heidelberg (2012), doi: 10.1007/978-3-642-31374-5_30
Cairns, P., Gow, J.: Using and parsing the Mizar language. Electronic Notes in Theoretical Computer Science 93, 60–69 (2004). doi: 10.1016/j.entcs.2003.12.028. http://www.sciencedirect.com/science/article/pii/S1571066104000131
Davis, M.: Obvious logical inferences. In: Proceedings of the Seventh International Joint Conference on Artificial Intelligence, pp. 530–531 (1981)
Giunchiglia, F., Walsh, T.: Theorem proving with definitions. In: Proceedings of AISB 89, pp. 433–435 (1989)
Grabowski, A., Naumowicz, A.: Mizar in a nutshell. J. Formal. Reasoning, Special Issue: User Tutorials I 3(2), 153–245 (2010)
Grabowski, A., Schwarzweller, C.: Translating mathematical vernacular into knowledge repositories. In: Proceedings of MKM’05, pp. 49–64. Springer-Verlag, Berlin, Heidelberg. doi: 10.1007/11618027_4 (2006)
Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Proceedings of Calculemus ’07 / MKM ’07, pp. 235–249. Springer-Verlag, Berlin, Heidelberg. doi: 10.1007/978-3-540-73086-6_20(2007)
Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Ganzha, M. et al. (eds.) FedCSIS 2012, Wroclaw, Poland, September 2012, Proceedings, pp. 63–68 (2012)
Grätzer, G.: General Lattice Theory. Academic Press, New York (1978)
Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar Mathematical Library in OMDoc Translation and applications. J. Autom. Reasoning 50(2), 191–202 (2013). doi: 10.1007/s10817-012-9271-4
Jaskowski, S.: On the Rules of Suppositions in Formal Logic. Studia Logica. Nakladem Seminarjum Filozoficznego Wydzialu Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego (1934). http://books.google.pl/books?id=6w0vRAAACAAJ
Kieffer, S., Avigad, J., Friedman, H.: A language for mathematical knowledge management. In: Grabowski, A. et al. (eds.) Computer Reconstruction of the Body of Mathematics, Studies in Logic, Grammar and Rhetoric, vol. 18(31), pp. 51–66. Bialystok (2009)
Kornilowicz, A.: On rewriting rules in Mizar. J. Autom. Reasoning 50(2), 203–210 (2013). doi: 10.1007/s10817-012-9261-6
Naumowicz, A.: Interfacing external CA systems for Grobner bases computation in Mizar proof checking. Int. J. Comput. Math. 87(1), 1–11 (2010). doi: 10.1080/00207160701864459
Naumowicz, A. In: Watt, S.M. et al. (eds.) : SAT-enhanced Mizar proof checking (2014). doi: 10.1007/978-3-319-08434-3_37
Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A. et al. (eds.) MKM 2004 Proceedings, LNCS, vol. 3119, pp. 290–301. doi: 10.1007/978-3-540-27818-4_21 (2004)
Naumowicz, A., Kornilowicz, A., et al.: A brief overview of Mizar. In: Berghofer, S. (ed.) Proceedings of TPHOLs’09, LNCS, vol. 5674, pp. 67–72. Springer-Verlag, Berlin, Heidelberg. doi: 10.1007/978-3-642-03359-9_5 (2009)
Pak, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reasoning 50(2), 217–228 (2013). doi: 10.1007/s10817-012-9267-0
Pak, K.: Improving legibility of natural deduction proofs is not trivial. Logical Methods in Comput. Sc. 10(3), 1–30 (2014). doi: 10.2168/LMCS-10(3:23)2014
Trybulec, A., Kornilowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. J. Autom. Reasoning 50(2), 119–121 (2013). doi: 10.1007/s10817-012-9268-z
Urban, J.: XML-izing Mizar: Making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) MKM 2005, Bremen, Germany July 2005, LNCS, vol. 3863, pp. 346–360 Springer . doi: 10.1007/11618027_23 (2005)
Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: Fukuda, K. et al. (eds.) ICMS 2010, Kobe, Japan. LNCS, vol. 6327, pp. 155–166. Springer. doi: 10.1007/978-3-642-15582-6_30 (2010)
In: Wiedijk, F. (ed.) : The Seventeen Provers of the World, Foreword by Dana S. Scott, LNCS, vol. 3600. Springer (2006)
Woronowicz, E.: Relations and their basic properties. Formalized Mathematics 1(1), 73–83 (1990). http://fm.mizar.org/1990-1/pdf1-1/relat_1.pdf
Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, Englewood Cliffs. N.J (1987)
Wos, L.: The problem of definition expansion and contraction. J. Autom. Reasoning 3(4), 433–435 (1987)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Korniłowicz, A. Definitional Expansions in Mizar. J Autom Reasoning 55, 257–268 (2015). https://doi.org/10.1007/s10817-015-9331-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9331-7