System Description: Xsl-Based Translator Of Mizar To Latex

Grzegorz Bancerek,Adam Naumowicz,Josef Urban

INTELLIGENT COMPUTER MATHEMATICS (CICM 2018)（2018）

引用 3|浏览35

暂无评分

摘要

We describe a new version of the Mizar-to-LATEX 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 LATEX/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.

查看译文

关键词

Mizar Mathematical Library (MML), Stylesheet, Mizar Authors, HTML Interpreter, Global Cutoff

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要