Skip to main content
SpringerLink
Log in

System Description: XSL-Based Translator of Mizar to LaTeX

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2018)

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

Included in the following conference series:

Abstract

We describe a new version of the Mizar-to- translator. The system has been re-implemented as XSL stylesheets instead of as Pascal programs, allowing greater flexibility. It can now be used to generate both /PDF and HTML with MathJax code. We also experimentally support generation of full proofs. Finally, the system is now available online and through the Mizar Emacs interface.

G. Bancerek—Deceased.

A. Naumowicz—Partially supported by the project N\(^\circ \) 2017/01/X/ST6/00012 financed by the National Science Center, Poland and the COST Action EUTypes CA15123. The Mizar processing has been performed using the infrastructure of the University of Bialystok High Performance Computing Center.

J. Urban—Supported by the ERC Consolidator grant no. 649043 AI4REASON, and by the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15 003/0000466 and the European Regional Development Fund.

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 EPUB and 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

Notes

  1. 1.

    https://www.degruyter.com/view/j/forma.

  2. 2.

    http://mizar.uwb.edu.pl/version/current/html/pcomps_2.html#K1, see also [6].

  3. 3.

    Both menu items trigger the mizar-tex-remote function in the current mizar.el Emacs Lisp mode for Mizar available at https://github.com/JUrban/mizarmode/blob/master/mizar.el.

References

  1. Bancerek, G.: Automatic translation in Formalized Mathematics. Mech. Math. Appl. 5(2), 19–31 (2006)

    Google Scholar 

  2. Bancerek, G.: Mizar analysis of algorithms: algorithms over integers. Formaliz. Math. 16(2), 177–194 (2008). https://doi.org/10.2478/v10037-008-0024-0

    Article  Google Scholar 

  3. Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, A., Pak, K.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1–4), 9–32 (2018). https://doi.org/10.1007/s10817-017-9440-6

    Article  MathSciNet  Google Scholar 

  4. Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17

    Chapter  Google Scholar 

  5. Bancerek, G., Carlson, P.: Mizar and the machine translation of mathematics documents. http://www.mizar.org/project/banc_carl93.ps

  6. Borys, L.: On paracompactness of metrizable spaces. Formaliz. Math. 3(1), 81–84 (1992). http://fm.mizar.org/1992-3/pdf3-1/pcomps_2.pdf

  7. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar - foreword. J. Autom. Reason. 55(3), 191–198 (2015). https://doi.org/10.1007/s10817-015-9345-1

    Article  MathSciNet  Google Scholar 

  8. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM - 2007. LNCS (LNAI), vol. 4573, pp. 235–249. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_20

    Chapter  MATH  Google Scholar 

  9. Naumowicz, A., Piliszek, R.: Accessing the Mizar library with a weakly strict Mizar parser. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 77–82. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_6

    Chapter  Google Scholar 

  10. Trybulec, A., Rudnicki, P.: A collection of TeXed Mizar abstracts. http://www.mizar.org/project/TR-89-18.pdf

  11. Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006). https://doi.org/10.1007/11618027_23

    Chapter  Google Scholar 

  12. Urban, J.: MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. 4(4), 414–427 (2006)

    Article  MathSciNet  Google Scholar 

  13. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reason. 50, 229–241 (2013). https://doi.org/10.1007/s10817-012-9269-y

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bialystok, Bialystok, Poland

    Adam Naumowicz

  2. Czech Technical University in Prague, Prague, Czech Republic

    Grzegorz Bancerek & Josef Urban

Authors
  1. Grzegorz Bancerek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Adam Naumowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Josef Urban
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adam Naumowicz .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Bayern, Germany

    Florian Rabe

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    William M. Farmer

  3. University of Cambridge, Cambridge, United Kingdom

    Grant O. Passmore

  4. Department of Computer Science, The George Washington University, Washington, District of Columbia, USA

    Abdou Youssef

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bancerek, G., Naumowicz, A., Urban, J. (2018). System Description: XSL-Based Translator of Mizar to LaTeX. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-96812-4_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-96811-7

  • Online ISBN: 978-3-319-96812-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation