Skip to main content
SpringerLink
Log in

OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge

  • Conference paper
  • First Online:
Artificial Intelligence and Symbolic Computation (AISC 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1930))

Abstract

In this paper we present an extension OMDoc to the Open- Math standard that allows the representation of the semantics and structure of various kinds of mathematical documents, including articles, textbooks, interactive books, courses. It can serve as the content language for agent communication of mathematical services on a mathematical software bus.

We will for the purposes of this paper subsume all of the implementations by the term MathWeb, since the communication protocols presented in this paper will make the constructions of bridges between the particular implementations simple, so that that the combined systems appear to the outside as one homogenous web.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Serge Autexier, Dieter Hutter, Heiko Mantel, and Axel Schairer. Towards an evolutionary formal software-development using CASL. In C. Choppy and D. Bert, editors, Proceedings Workshop on Algebraic Development Techniques, WADT-99. Springer, LNCS 1827, 2000.

    Google Scholar 

  2. Alessandro Armando and Michael Kohlhase. Communication protocols for mathematical services based on KQML and OMRS. In Manfred Kerber and Michael Kohlhase, editors, CALCULEMUS-2000, Systems for Integrated Computation and Deduction, 2000, AKPeters.

    Google Scholar 

  3. [AvLS96] J. Abbot, A. van Leeuwen, and A. Strotmann. Objectives of Open-Math. Technical report 12, RIACA, Technische Universiteit Eindhoven, The Netherlands, June 1996.

    Google Scholar 

  4. Alessandro Armando and Daniele Zini. Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture. In A. Poggi, editor, AI*IA-TABOO Workshop ‘From Objects to Agents: Evolutionary Trends of Software Systems’, 2000.

    Google Scholar 

  5. Judith Baur. Syntax und semantik mathematisher texte—ein prototyp. Master Thesis, Saarland University, 1999.

    Google Scholar 

  6. Christoph Benzmüller, Matthew Bishop, and Volker Sorge. Integrating Tps and Ωmega. Journal of Universal Computer Science, 5(2), 1999.

    Google Scholar 

  7. The Ωmega group. Ωmega: Towards a mathematical assistant. In William McCune, editor, CADE-14, LNAI 1249, pages 252–255, 1997. Springer Verlag.

    Google Scholar 

  8. Tim Bray, Jean Paoli, and C. M. Sperberg-McQueen. Extensible Markup Language (XML). W3C Recommendation TR-XML, December 1997. http://www.w3.org/tr/pr-xml.html.

  9. Robert G. Bartle and Donald Sherbert. Introduction to Real Analysis. Wiley, 2 edition, 1982.

    Google Scholar 

  10. R. Boulton, K. Slind, A. Bundy, and M. Gordon. An interface between CLAM and HOL. In Jim Grundy and Malcolm Newey, editors, TPHOLS-98, pages 87–104, 1998.

    Google Scholar 

  11. Olga Caprotti and Arjeh M. Cohen. Draft of the OpenMath standard. The Open Math Society, http://www.nag.co.uk/projects/openmath/omstd/, 1998.

    Google Scholar 

  12. Arjeh Cohen, Hans Cuypers, and Hans Sterk. Algebra Interactive! Springer Verlag, 1999. Interactive Book on CD.

    Google Scholar 

  13. Language Design Task Group CoFI. Casl-the CoFI algebraic specification language-summary, version 1.0. Technical report, http://www.brics.dk/projects/cofi, 1998.

  14. Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, and Tom Melham. The Prosper toolkit. In Proc. TACAS-2000, 2000.

    Google Scholar 

  15. Stephen Deach. Extensible stylesheet language (xsl) specification. W3c working draft, W3C, 1999. http://www.w3.org/TR/WD-xsl.

  16. T. Finin and R. Fritzson. KQML—a language and protocol for knowledge and information exchange. In Proceedings of the 13th Intl. Distributed Artificial Intelligence Workshop, pages 127–136, 1994.

    Google Scholar 

  17. Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, and Volker Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 5:156–187, 1999.

    MATH  Google Scholar 

  18. Armin Fiedler. Towards a proof explainer. In Siekmann et al. [SPH97], pages 53–54.

    Google Scholar 

  19. Armin Fiedler. Using a cognitive architecture to plan dialogs for the adaptive explanation of proofs. In Thomas Dean, editor, Proceedings IJCAI-99, pages 358–363, 1999. Morgan Kaufmann.

    Google Scholar 

  20. Andreas Franke and Michael Kohlhase. Communicating with MBASE in KQML. Internet Draft http://www.mathweb.org/mbase, 1999.

  21. Andreas Franke and Michael Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Harald Ganzinger, editor, Proceedings CADE-16, LNAI 1632, pages 217–221. Springer Verlag, 1999.

    Google Scholar 

  22. Andreas Franke and Michael Kohlhase. System description: MBase, an open mathematical knowledge base. In David McAllester, editor, CADE-17, LNAI 1831, pages 455–459. Springer Verlag, 2000.

    Google Scholar 

  23. Xiaorong Huang and Armin Fiedler. Presenting machine-found proofs. In M.A. McRobbie and J.K. Slaney, editors, Proceedings CADE-13, LNAI 1104, pages 221–225, 1996. Springer Verlag.

    Google Scholar 

  24. Xiaorong Huang and Armin Fiedler. Proof verbalization in PROVERB. In Siekmann et al. [SPH97], pages 35–36.

    Google Scholar 

  25. Helmut Horacek. Generating inference-rich discourse through revisions of RST-trees. In Proceedings AAAI-98, pages 814–820. MIT Press, 1998.

    Google Scholar 

  26. Dieter Hutter. Reasoning about theories. Technical report, DFKI, 1999.

    Google Scholar 

  27. Patrick Ion and Robert Miner. Mathematical Markup Language (MathML) 1.0 specification. W3C Recommendation 1998. http://www.w3.org/TR/REC-MathML/.

  28. Michael Kohlhase and Andreas Franke. Mbase: Representing knowledge and context for the integration of mathematical software systems. Journal of Symbolic Comutation, 2000. forthcoming.

    Google Scholar 

  29. Michael Kohlhase. Creating omdoc representations from LATEX. Internet Draft http://www.mathweb.org/omdoc, 2000.

  30. Michael Kohlhase. OMDoc: Towards an openmath representation of mathematical documents. Seki Report SR-00-02, Fachbereich Informatik, UniversitÄt des Saarlandes, 2000.

    Google Scholar 

  31. William Mann and Sandra Thompson. Rhethorical structure theory: A theory of text organization. Technical Report ISI/RR-83-115, ISI at University of Southern California, 1983.

    Google Scholar 

  32. Dave Raggett, Arnaud Le Hors, and IanJacobs. HTML 4.0 Specification. W3C Recommendation 1998. http://www.w3.org/TR/PR-xml.html.

  33. Martin Schönert et al. GAP–Groups, Algorithms, and Programming. RWTH Aachen, Germany, 1995.

    Google Scholar 

  34. [SBC+00] The Ωmega group. Adaptive course generation and presentation. In P. Brusilovski, editor, Proceedings of ITS-2000 workshop on Adaptive and Intelligent Web-Based Education Systems, Montreal, 2000.

    Google Scholar 

  35. Y. Shoham. Agent-Oriented Programming. Technical report, Stanford University, 1990.

    Google Scholar 

  36. M. Kohlhase S. Hess, Ch. Jung and V. Sorge. An implementation of distributed mathematical services. In Arjeh Cohen and Henk Barendregt, editors, CALCULEMUS and TYPES, 1998.

    Google Scholar 

  37. J. Siekmann, F. Pfenning, and X. Huang, editors. Proceedings of the First International Workshop on Proof Transformation and Presentation, Schloss Dagstuhl, Germany, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FB Informatik, Universität des Saarlandes, Saarbrücken

    Michael Kohlhase

Authors
  1. Michael Kohlhase
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University College London, Gower Street, WC1E 6BT, London, UK

    John A. Campbell

  2. Dept. Algebra, Fac. Educación, Universidad Complutense de Madrid, c/Rector Royo Villanova s/n, 28040, Madrid, Spain

    Eugenio Roanes-Lozano

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kohlhase, M. (2001). OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge. In: Campbell, J.A., Roanes-Lozano, E. (eds) Artificial Intelligence and Symbolic Computation. AISC 2000. Lecture Notes in Computer Science(), vol 1930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44990-6_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-44990-6_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42071-2

  • Online ISBN: 978-3-540-44990-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation