Skip to main content
SpringerLink
Log in

MathLang Translation to Isabelle Syntax

  • Conference paper
Intelligent Computer Mathematics (CICM 2009)

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

Included in the following conference series:

  • 764 Accesses

Abstract

Converting mathematical documents from a human-friendly natural language to a form that can be readily processed by computers is often a tedious, manual task. Translating between varied computerised forms is also a difficult problem. MathLang, a system of methods and representations for computerising mathematics, tries to make these tasks more tractable by breaking the translation down into manageable portions. This paper presents a method for creating rules to translate documents from MathLang’s internal representation of mathematics to documents in the language of the Isabelle proof assistant. It includes a set of example rules applicable for a particular document. The resulting documents are not completely verifiable by Isabelle, but they represent a point to which a mathematician may take a document without the involvement of an Isabelle expert.

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. Kamareddine, F., Lamar, R., Maarek, M., Wells, J.B.: Restoring natural language as a computerised mathematics input method. In: MKM 2007 [20], pp. 280–295 (2007)

    Google Scholar 

  2. Kamareddine, F., Maarek, M., Wells, J.B.: Toward an object-oriented structure for mathematical text. In: Kohlhase, M. (ed.) MKM 2005. LNCS, vol. 3863, pp. 217–233. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Kamareddine, F., Maarek, M., Retel, K., Wells, J.B.: Narrative structure of mathematical texts. In: MKM 2007 [20], pp. 296–311 (2007)

    Google Scholar 

  4. Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs (1992)

    Google Scholar 

  5. Buchberger, B., Crǎciun, A., Jebelean, T., Kovács, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards Computer-Aided Mathematical Theory Exploration. Journal of Applied Logic, 470–504 (2006)

    Google Scholar 

  6. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  7. Wenzel, M.T.: Isar – a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–184. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Humayoun, M.: Software specifications and mathematical proofs in natural languages. Poster in Journées scientifiques du cluster, ISLE Rhône-Alpes, Domaine universitaire, Grenoble, France (2008)

    Google Scholar 

  9. Ranta, A.: Grammatical framework: A type-theoretical grammar formalism. Journal of Functional Programming 14(2), 145–189 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  10. Heath, T.L.: The 13 Books of Euclid’s Elements. Dover, New York (1956); in 3 volumes. Sir Thomas Heath originally published this in 1908

    Google Scholar 

  11. Landau, E.: Grundlagen der Analysis. Chelsea (1930)

    Google Scholar 

  12. LogiCal Project, INRIA, Rocquencourt, France. The Coq Proof Assistant Reference Manual – Version 8.0 (June 2004), ftp://ftp.inria.fr/INRIA/coq/V8.0/doc/

  13. Grue, K.: The layers of Logiweb. In: Towards Mechanized Mathematical Assistants (Calculemus 2007 and MKM 2007 Joint Proceedings), pp. 250–264 (2007)

    Google Scholar 

  14. Knuth, D.E., Levy, S.: The CWEB System of Structured Documentation: Version 3.0. Addison-Wesley/ Longman Publishing Co., Inc., Boston (1994)

    Google Scholar 

  15. Gallian, J.A.: Contemporary Abstract Algebra, 5th edn. Houghton Mifflin Company (2002)

    Google Scholar 

  16. Kamareddine, F., Wells, J.B.: Computerizing mathematical text with MathLang. In: Ayala-Rincon, M., Heusler (eds.) Proc. Second Workshop on Logical and Semantic Frameworks, with Applications, Ouro Preto, Minas Gerais, Brazil, pp. 5–30. Elsevier, Amsterdam (2008); The LSFA 2007 (post-event) proceedings is published as vol. 205 (2008-04-06) Elec. Notes in Theoret. Comp. Sci.

    Google Scholar 

  17. Maarek, M.: Mathematical Documents Faithfully Computerised: the Grammatical and Text & Symbol Aspects of the MathLang Framework. PhD thesis, Heriot-Watt University, Edinburgh, Scotland (June 2007)

    Google Scholar 

  18. Clark, J., DeRose, S.: XML Path Language (XPath) Version 1.0. W3C (World Wide Web Consortium) (1999), http://www.w3.org/TR/xpath

  19. Chaieb, A.: Semiring normalization and Groebner bases. File Groebner_Basis.thy, in Isabelle2007 distribution (October 2007)

    Google Scholar 

  20. Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.): MKM/Calculemus 2007. LNCS (LNAI), vol. 4573. Springer, Heidelberg (2007)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ULTRA Group, Heriot-Watt University, UK

    Robert Lamar, Fairouz Kamareddine & J. B. Wells

Authors
  1. Robert Lamar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fairouz Kamareddine
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. B. Wells
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada

    Jacques Carette

  2. Informatics, 2.02 Informatics Forum, University of Edinburgh, 10 Crichton street, EH8 9AB, Edinburgh, UK

    Lucas Dixon

  3. Department of Computer Science, University of Bologna, via Mura Anteo Zamboni, 7, 40127, Bologna, Italy

    Claudio Sacerdoti Coen

  4. Department of Computer Science MC 375, University of Western Ontario, N6A 5B7, London, ON, Canada

    Stephen M. Watt

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lamar, R., Kamareddine, F., Wells, J.B. (2009). MathLang Translation to Isabelle Syntax. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds) Intelligent Computer Mathematics. CICM 2009. Lecture Notes in Computer Science(), vol 5625. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02614-0_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02614-0_30

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02613-3

  • Online ISBN: 978-3-642-02614-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation