Abstract
Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the semantics in programming languages and emphasize computation. Combining the complementary strengths of both approaches while mending their complementary weaknesses has been an important goal of the mechanized mathematics community for some time.
We pick up on the idea of biform theories and interpret it in the Mmt/ OMDoc framework which introduced the foundations-as-theories approach, and can thus represent both logics and programming languages as theories. This yields a formal, modular framework of biform theory graphs which mixes specifications and implementations sharing the module system and typing information.
We present automated knowledge management work flows that interface to existing specification/programming tools and enable an OpenMath Machine, that operationalizes biform theories, evaluating expressions by exhaustively applying the implementations of the respective operators. We evaluate the new biform framework by adding implementations to the OpenMath standard content dictionaries.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.: The KeY Tool. Software and System Modeling 4, 32–54 (2005)
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), http://www.openmath.org/standard/om20
Boespflug, M., Carbonneaux, Q., Hermant, O.: The λΠ-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP 2012: Proof Exchange for Theorem Proving, pp. 28–43 (2012)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)
Davenport, J.: A small OpenMath type system. Bulletin of the ACM Special Interest Group on Symbolic and Automated Mathematics (SIGSAM) 34(2), 16–21 (2000)
Delahaye, D., Mayero, M.: Dealing with Algebraic Expressions over a Field in Coq using Maple. Journal of Symbolic Computation 39(5), 569–592 (2005)
Farmer, W.M.: Biform theories in chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 66–79. Springer, Heidelberg (2007)
Farmer, W., Guttman, J., Thayer, F.: Little Theories. In: Kapur, D. (ed.) Conference on Automated Deduction, pp. 467–581 (1992)
Hardin, T., et al.: The focalize essential (2012), http://focalize.inria.fr/
Horozal, F., Iacob, A., Jucovschi, C., Kohlhase, M., Rabe, F.: Combining Source, Content, Presentation, Narration, and Relational Representation. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS, vol. 6824, pp. 212–227. Springer, Heidelberg (2011)
Haftmann, F., Nipkow, T.: Code Generation via Higher-Order Rewrite Systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010)
Heras, J., Pascual, V., Romero, A., Rubio, J.: Integrating Multiple Sources to Answer Questions in Algebraic Topology. 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. 331–335. Springer, Heidelberg (2010)
Harrison, J., Théry, L.: A Skeptic’s Approach to Combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)
Kohlhase, M., Rabe, F.: Semantics of OpenMath and MathML3. Mathematics in Computer Science 6(3), 235–260 (2012)
Kahrs, S., Sannella, D., Tarlecki, A.: The definition of extended ML: A gentle introduction. Theoretical Computer Science 173(2), 445–484 (1997)
Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
OpenMath Content Dictionaries, http://www.openmath.org/cd/
Odersky, M., Spoon, L., Venners, B.: Programming in Scala. artima (2007)
Rabe, F.: A Logical Framework Combining Model and Proof Theory. Mathematical Structures in Computer Science (to appear, 2013), http://kwarc.info/frabe/Research/rabe_combining_10.pdf
Rabe, F.: The MMT API: A Generic MKM System. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 339–343. Springer, Heidelberg (2013)
Rabe, F., Kohlhase, M.: A Scalable Module System. Information and Computation (2013), conditionally accepted http://arxiv.org/abs/1105.0548
The Coq Development Team. The coq proof assistant: Reference manual. Technical report, INRIA (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kohlhase, M., Mance, F., Rabe, F. (2013). A Universal Machine for Biform Theory Graphs. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds) Intelligent Computer Mathematics. CICM 2013. Lecture Notes in Computer Science(), vol 7961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39320-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-39320-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39319-8
Online ISBN: 978-3-642-39320-4
eBook Packages: Computer ScienceComputer Science (R0)