zbMATH — the first resource for mathematics

A web-based toolkit for mathematical word processing applications with semantics. (English) Zbl 1367.68332
Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 272-291 (2017).
Summary: Lurch is an open-source word processor that can check the steps in students’ mathematical proofs. Users write in a natural language, but mark portions of a document as meaningful, so the software can distinguish content for human readers from content it should analyze.
This paper describes the Lurch Web Platform, a system of tools the authors have created as part of a project to upgrade Lurch from a desktop application to a web application. That system of tools is available on GitHub for other mathematical software developers to use in their own projects. It includes a web editor with mathematical typesetting, an interface for marking up documents with mathematical (or other structured) meaning, OpenMath support, meaning visualization tools, and document dependence and sharing features, among others.
We conclude with design plans for ongoing development of the web version of Lurch that will be built on the Lurch Web Platform.
For the entire collection see [Zbl 1364.68010].

68U15 Computing methodologies for text processing; mathematical typography
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
Full Text: DOI
[1] Ashkenas, J.: Literate CoffeeScript, February 2013. http://coffeescript.org/#literate
[2] Beezer, R.A.: MathBook XML Author’s Guide, March 2017. http://mathbook.pugetsound.edu/doc/author-guide/mathbook-author-guide.pdf
[3] Carter, N.: jsfs: a (small) filesystem stored in the browser’s LocalStorage. A free and open source software project, May 2015. http://github.com/nathancarter/jsfs
[4] Carter, N., Monks, K.G.: Introduction to Lurch: advanced users guide (2012). http://lurchmath.org/AUG-v1.html
[5] Carter, N., Monks, K.G.: Lurch: a word processor built on OpenMath that can check mathematical reasoning. In: Lange, C., et al. (eds.) Workshops and Work in Progress at CICM, EEEE 1010. CEUR Workshop Proceedings (2013)
[6] Carter, N., Monks, K.G.: Lurch: a word processor that can grade students’ proofs. In: Lange, C., et al. (eds.) Workshops and Work in Progress at CICM, FFFFF 1010. CEUR Workshop Proceedings (2013)
[7] Carter, N., Monks, K.G.: From formal to expository: using the proof-checking word processor Lurch to teach proof writing. In: Schwell, R., Franko, J., Steurer, A. (eds.) Beyond Lecture: Resources and Pedagogical Techniques for Enhancing the Teaching of Proof-Writing Across the Curriculum. Mathematical Association of America (2015)
[8] Carter, N., Monks, K.G.: Lurch: a word processor that can check your math. A free and open source software project, March 2017. http://lurchmath.org
[9] Carter, N., Monks, K.G.: webLurch: a web-based word processor that can check your math. A free and open source software project under development, March 2017. http://nathancarter.github.io/weblurch
[10] Carter, N., Monks, K.G.: GitHub repository for the webLurch project (2017). https://github.com/nathancarter/weblurch
[11] Cervone, D., et al.: MathJax: beautiful math in all browsers. A free and open source software project (2017). http://mathjax.org
[12] The Coq Development Team: The Coq proof assistant reference manual version 0.8 (2004). http://coq.inria.fr
[13] Microsoft Corporation: Microsoft office support: write an equation (2017). https://support.office.com/en-us/article/Write-an-equation-88e01bd4-54c5-4cf7-af83-8601084bf919
[14] de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover. In: 25th International Conference on Automated Deduction (CADE-25) (2015) · Zbl 06515520
[15] Gruber, J.: Markdown, December 2004. https://daringfireball.net/projects/markdown/
[16] Harrison, J.: The HOL Light system reference, October 2016. https://github.com/jrh13/hol-light/
[17] Kahl, W.: The teaching tool CalcCheck a proof-checker for Gries and Schneider’s ”Logical Approach to Discrete Math”. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 216–230. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-25379-9_17 · Zbl 1350.68238 · doi:10.1007/978-3-642-25379-9_17
[18] TinyMCE, J.L., et al.: JavaScript WYSIWYG editor. A free and open source software project (2017). http://tinymce.com
[19] MediaWiki: Extension:articleprotection – MediaWiki, the free wiki engine (2015). https://www.mediawiki.org/w/index.php?title=Extension:ArticleProtection&oldid=1487335
[20] MediaWiki: MediaWiki – MediaWiki, the free wiki engine (2016). http://www.mediawiki.org/
[21] Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04652-0_5 · Zbl 1263.68038 · doi:10.1007/978-3-642-04652-0_5
[22] Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013) · Zbl 1358.68283 · doi:10.1016/j.ic.2013.06.001
[23] Seoul-Oh, H., Adkisson, J.: MathQuill: WYSIWYG math with only HTML, CSS, and JS. A free and open source software project, February 2017. http://mathquill.com
[24] The jQuery Foundation: jQuery API Documentation, June 2016. https://api.jquery.com/
[25] The LyX Team: LyX 1.6.1 - The Document Processor [Computer software and manual]. Internet (2009). http://www.lyx.org
. Accessed 16 Feb 2009
[26] Wenzel, M., Wol, B.: Isabelle/PIDE as platform for educational tools. In: Workshop on Computer Theorem Proving Components for Educational Software (THedu 2011). Electronic Proceedings in Theoretical Computer Science, vol. 79 (2012). doi: 10.4204/EPTCS.79.9 · doi:10.4204/EPTCS.79.9
[27] The World Wide Web Consortium: Cross-origin resource sharing, W3C recommendation 16, January 2014. https://www.w3.org/TR/cors/
[28] The World Wide Web Consortium: Web workers, W3C working draft 24, September 2015. https://www.w3.org/TR/2015/WD-workers-20150924/
[29] Velleman, D.J.: Variable declarations in natural deduction. Ann. Pure Appl. Logic 144(1–3), 133–146 (2006). doi: 10.1016/j.apal.2006.05.009 · Zbl 1115.03078 · doi:10.1016/j.apal.2006.05.009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.