Abstract
Throughout the twentieth century, the automation of formal logics in computers has created unprecedented potential for practical applications of logic—most prominently the mechanical verification of mathematics and software. But the high cost of these applications makes them infeasible but for a few flagship projects, and even those are negligible compared to the ever-rising needs for verification. One of the biggest challenges in the future of logic will be to enable applications at much larger scales and simultaneously at much lower costs. This will require a far more efficient allocation of resources. Wherever possible, theoretical and practical results must be formulated generically so that they can be instantiated to arbitrary logics; this will allow reusing results in the face of today’s multitude of application-oriented and therefore diverging logical systems. Moreover, the software engineering problems concerning automation support must be decoupled from the theoretical problems of designing logics and calculi; this will allow researchers outside or at the fringe of logic to contribute scalable logic-independent tools. Anticipating these needs, the author has developed the Mmt framework. It offers a modern approach towards defining, analyzing, implementing, and applying logics that focuses on modular design and logic-independent results. This paper summarizes the ideas behind and the results about Mmt. It focuses on showing how Mmt. provides a theoretical and practical framework for the future of logic.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Anonymous: The QED Manifesto. In: Bundy, A. (ed.) Automated Deduction, pp. 238–251. Springer, New York (1994)
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: Crafting a proof assistant. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, pp. 18–32. Springer, Berlin, Heidelberg (2007)
Ausbrooks, R., Buswell, S., Carlisle, D., Dalmas, S., Devitt, S., Diaz, A., Froumentin, M., Hunter, R., Ion, P., Kohlhase, M., Miner, R., Poppelier, N., Smith, B., Soiffer, N., Sutor, R., Watt, S.: Mathematical Markup Language (MathML) Version 2.0 (2nd edition), (2003). See http://www.w3.org/TR/MathML2
Boespflug, M., Carbonneaux, Q., Hermant, O.: The \({\lambda\Pi}\)-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28–43 (2012)
Buswell, S., Caprotti, O., Carlisle, D., Dewar, M., Gaetano, M., Kohlhase, M.: The Open Math Standard, Version 2.0. Technical report, The Open Math Society (2004). See http://www.openmath.org/standard/om20
Church A.: A formulation of the simple theory of types. J. Symbol. L. 5(1), 56–68 (1940)
Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project Abstract: logic atlas and integrator (LATIN). In: Davenport, J., Farmer, W., Urban, J., Rabe, F. (eds.) Intelligent Computer Mathematics, pp. 289–291. Springer, Berlin, Heidelberg (2011)
Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Upper Saddle River (1986)
Coq Development Team. The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S. R. (ed.) Typed Lambda Calculi and Applications, pp. 102–117. Springer, Berlin, Heidelberg (2007)
Curry, H., Feys, R.: Combinatory Logic. North-Holland, Amsterdam (1958)
Diaconescu R.: Institution-independent Model Theory. Birkhäuser, Geneva (2008)
Emir, B., Odersky, M., Williams, J.: Matching objects with patterns. In: Ernst, E. (ed.) European Conference on Object-Oriented Programming, pp. 273–298. Springer, New York (2007)
Goguen J., Burstall R.: Institutions: abstract model theory for specification and programming. J. Assoc. Comput. Mach. 39(1), 95–146 (1992)
Gordon, M.: HOL: a proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, pp. 73–128. Kluwer-Academic Publishers, Berlin (1988)
Hales, T., Adams, M., Bauer, G., Tat Dang, D., Harrison, J., Le Hoang, T., Kaliszyk, C., Magron, V., McLaughlin, S., Tat Nguyen, T., Quang Nguyen, T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A. Thi Ta, A., Nam Tran, T., Thi Trieu, D., Urban, J., Khac Vu, K., Zumkeller, R.: A formal proof of the Kepler conjecture, (2014). arxiv:1501.02155
Harper R., Honsell F., Plotkin G.: A framework for defining logics. J. Assoc. Comput. Mach., 40(1), 143–184 (1993)
Harrison, J.: HOL light: a tutorial introduction. In: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pp. 265–269. Springer, New York (1996)
HOL4 Development Team. http://hol.sourceforge.net/
Horozal F., Rabe F.: Representing model theory in a type-theoretical logical framework. Theor. Comput. Sci. 412(37), 4919–4945 (2011)
Howard, W.: The formulas-as-types notion of construction. In: To Curry, H.B.(ed.) Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479–490. Academic Press, Waltham (1980)
Iancu, M., Jucovschi, C., Kohlhase, M., Wiesing, T.: System description: MathHub.info. In: Watt, S., Davenport, J., Sexton, A., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, pp. 431–434. Springer, New York (2014)
Iancu M., Kohlhase M., Rabe F., Urban J.: The Mizar mathematical library in OMDoc: translation and applications. J. Auto. Reason. 50(2), 191–202 (2013)
Iancu M., Rabe F.: Formalizing foundations of mathematics. Math. Struct. Comput. Sci. 21(4), 883–911 (2011)
Iancu, M., Rabe, F.: Management of change in declarative languages. In: Campbell, J., Carette, J., Dos Reis, G., Jeuring, J., Sojka, P., Sorge, V., Wenzel, M. (eds.) Intelligent Computer Mathematics, pp. 325–340. Springer, New York (2012)
Kaliszyk, C., Rabe, F.: Towards knowledge management for HOL light. In: Watt, S., Davenport, J., Sexton, A., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, pp. 357–372. Springer, New York (2014)
Kaufmann M., Manolios P., Moore J.: Computer-Aided Reasoning: An Approach. Academic Publishers, Berlin (2000)
Klein G., Andronick J., Elphinstone K., Heiser G., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)
Kohlhase M.: OMDoc: an open markup format for mathematical documents (Version 1.2). Number 4180 in Lecture Notes in Artificial Intelligence. Springer, New York (2006)
Kohlhase, M., Şucan, I.: A search engine for mathematical formulae. In: Ida, T., Calmet, J., Wang, D. (eds.) Artificial Intelligence and Symbolic Computation, pp. 241–253. Springer, New York (2006)
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems 2007. Lecture Notes in Computer Science, volume 4424, pp. 519–522 (2007)
Nipkow T., Paulson L., Wenzel M.: Isabelle/HOL: a proof assistant for higher-order logic, Springer. Springer, New York (2002)
Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE), pp. 748–752. Springer, New York (1992)
Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science. Volume 828, Springer, New York (1994)
Pfenning, F.: Logical frameworks. In: Robinson, J., Voronkov, A. (eds.) Handbook of automated reasoning, pp. 1063–1147. Elsevier, Amsterdam (2001)
Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated deduction, pp. 202–206 (1999)
Rabe, F.: A query language for formal mathematical libraries. In: Campbell, J., Carette, J., Dos Reis, G., Jeuring, J., Sojka, P., Sorge, V., Wenzel, M. (eds.) Intelligent Computer Mathematics, pp. 142–157. Springer, New York (2012)
Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics, pp. 339–343. Springer, New York (2013)
Rabe, F.: A logic-independent IDE. In: Benzmller, C., Woltzenlogel Paleo, B. (eds.) Workshop on User Interfaces for Theorem Provers, pages 48–60. Elsevier, Amsterdam (2014)
Rabe, F.: How to identify, translate, and combine logics? J. Logic Comput. (2014). doi:10.1093/logcom/exu079
Rabe, F.: Generic literals. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics, pp. 102–117. Springer, New York (2015)
Rabe, F.: Theory Expressions: A Survey (2015). http://kwarc.info/frabe/Research/rabe_theoexp_15.pdf
Rabe F., Kohlhase M.: A scalable module system. Inf. Comput. 230(1), 1–54 (2013)
Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28. Morgan Kaufmann, Burlington (1985)
Author information
Authors and Affiliations
Corresponding author
Additional information
The author was supported by DFG Grant RA-18723-1 OAF.
This paper won the prize of the UNILOG’2015 contest, The Future of Logic: http://www.uni-log.org/future-of-logic.
Rights and permissions
About this article
Cite this article
Rabe, F. The Future of Logic: Foundation-Independence. Log. Univers. 10, 1–20 (2016). https://doi.org/10.1007/s11787-015-0132-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-015-0132-x