Abstract
This paper presents a combination of several automated reasoning and proof presentation tools with the Mizar system for formalization of mathematics. The combination forms an online service called MizAR, similar to the SystemOnTPTP service for first-order automated reasoning. The main differences to SystemOnTPTP are the use of the Mizar language that is oriented towards human mathematicians (rather than the pure first-order logic used in SystemOnTPTP), and setting the service in the context of the large Mizar Mathematical Library of previous theorems, definitions, and proofs (rather than the isolated problems that are solved in SystemOnTPTP). These differences poses new challenges and new opportunities for automated reasoning and for proof presentation tools. This paper describes the overall structure of MizAR, and presents the automated reasoning systems and proof presentation tools that are combined to make MizAR a useful mathematical service.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Automate Reasoning
- Proof Assistant
- Automate Theorem Prove
- Mizar Mathematical Library
- Automate Theorem Prove System
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bancerek, G.: The Ordinal Numbers. Journal of Formalized Mathematics 1(1), 91–96 (1990)
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)
Benzmüller, C., Paulson, L.: Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL (2010)
Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: Lightweight Integration of the Ergo Theorem Prover Inside a Proof Assistant. In: Rushby, J., Shankar, N. (eds.) Proceedings of the 2nd Workshop on Automated Formal Methods, pp. 55–59. ACM Press, New York (2007)
Corbineau, P., Geuvers, H., Kaliszyk, C., McKinna, J., Wiedijk, F.: A Real Semantic Web for Mathematics Deserves a Real Semantics. In: Lange, C., Schaffert, S., Skaf-Molli, H., Völkel, M. (eds.) Proceedings of the 3rd Semantic Wiki Workshop. CEUR Workshop Proceedings, vol. 360, pp. 62–66 (2008)
Corbineau, P., Kaliszyk, C.: Cooperative Repositories for Formal Proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 221–234. Springer, Heidelberg (2007)
D’Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems 27(7), 1165–1178 (2008)
Gonthier, G.: Formal Proof - The Four-Color Theorem. Notices of the American Mathematical Society 55(11), 1382–1393 (2008)
Hales, T.: A Proof of the Kepler Conjecture. Annals of Mathematics 162(3), 1065–1185 (2005)
Hales, T. (ed.): A Special Issue on Formal Proof, vol. 55 (2008)
Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Archer, M., Di Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics. number NASA/CP-2003-212448 NASA Technical Reports, pp. 56–68 (2003)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal Verification of an OS Kernel. In: Anderson, T. (ed.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pp. 207–220. ACM Press, New York (2009)
Kotowicz, J., Raczkowski, K.: Real Function Differentiability - Part II. Formalized Mathematics 2(3), 407–411 (1991)
McCune, W.W.: Solution of the Robbins Problem. Journal of Automated Reasoning 19(3), 263–276 (1997)
Paulson, L.: A Generic Tableau Prover and its Integration with Isabelle. Artificial Intelligence 5(3), 73–87 (1999)
Pease, A., Sutcliffe, G.: First Order Reasoning on a Large Ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. CEUR Workshop Proceedings, vol. 257, pp. 59–69 (2007)
Phillips, J.D., Stanovsky, D.: Automated Theorem Proving in Loop Theory. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics. CEUR Workshop Proceedings, vol. 378, pp. 42–53 (2008)
Puzis, Y., Gao, Y., Sutcliffe, G.: Automated Generation of Interesting Theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49–54. AAAI Press, Menlo Park (2006)
Raczkowski, K., Sadowski, P.: Real Function Differentiability. Formalized Mathematics 1(4), 797–801 (1990)
Schulz, S.: E: A Brainiac Theorem Prover. AI Communications 15(2-3), 111–126 (2002)
Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., de Melo, G.: External Sources of Axioms in Automated Theorem Proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS (LNAI), vol. 5803, pp. 281–288. Springer, Heidelberg (2009)
Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 406–410. Springer, Heidelberg (2000)
Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools 15(6), 1053–1070 (2006)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)
Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67–81. Springer, Heidelberg (2006)
Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp. 341–345. AAAI Press, Menlo Park (1999)
Sutcliffe, G., Yerikalapudi, A., Trac, S.: Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems. In: Guesgen, H., Lane, C. (eds.) Proceedings of the 22nd International FLAIRS Conference, pp. 105–110. AAAI Press, Menlo Park (2009)
Trac, S., Puzis, Y., Sutcliffe, G.: An Interactive Derivation Viewer. In: Autexier, S., Benzmüller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol. 174, pp. 109–123 (2006)
Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentaion of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006)
Urban, J.: MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics. Journal of Applied Logic 4(4), 414–427 (2006)
Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning 37(1-2), 21–43 (2006)
Urban, J.: Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics. CEUR Workshop Proceedings, vol. 418, pp. 1–16 (2008)
Urban, J., Sutcliffe, G.: ATP-based Cross Verification of Mizar Proofs: Method, Systems, and First Experiments. Journal of Mathematics in Computer Science 2(2), 231–251 (2009)
Urban, J., Sutcliffe, G., Pudlak, P., Vyskocil, J.: MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008)
Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP Semantic Presentation and Verification Tools. Studies in Logic, Grammar and Rhetoric 18(31), 121–136 (2009)
Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: SPASS Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 514–520. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urban, J., Sutcliffe, G. (2010). Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-14128-7_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14127-0
Online ISBN: 978-3-642-14128-7
eBook Packages: Computer ScienceComputer Science (R0)