OMDoc – An Open Markup Format for Mathematical Documents [version 1.2]
Foreword by Allan Bundy
Article
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the l...
Chapter and Conference Paper
Mathematicians integrate acquired knowledge into a mental model. For trained mathematicians, the mental model seems to include not just the bare facts, but various induced forms of knowledge, and the amount of...
Chapter and Conference Paper
In the traditional knowledge dissemination process in mathematics and sciences, authors write semi-selfcontained articles which are then published in journals, conference proceedings, preprint archives, and/or...
Chapter and Conference Paper
We present the MathHub.info system, a development environment for active mathematical documents and an archive for flexiformal mathematics. It offers a rich interface for reading, writing, and interacting with ma...
Chapter and Conference Paper
We present a to-Office conversion plugin for ML that can bri...
Chapter and Conference Paper
To understand mathematical language we have to understand the words of mathematics. In particular, for machine-supported knowledge management and digital libraries, we need machine-actionable terminology datab...
Chapter and Conference Paper
Since there are different ways of axiomatizing and develo** a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We i...
Chapter and Conference Paper
We study representation formats that allow formally defining what we call flexary operators: functions that take arbitrarily many arguments, like ...
Article
The Mizar Mathematical Library is one of the largest libraries of formalized and mechanically verified mathematics. Its language is highly optimized for authoring by humans. As in natural languages, the meaning o...
Chapter and Conference Paper
Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the sema...
Chapter and Conference Paper
The Planetary develops a general framework – the Planetary – for social semantic portals that support users in interacting with STEM (Science/Technology/Engineering/Mathematics) documents. Developed from an initi...
Chapter and Conference Paper
The Mathematics Subject Classification (MSC) is a widely used scheme for classifying documents in mathematics by subject. Its traditional, idiosyncratic conceptualization and representation makes the scheme ha...
Chapter and Conference Paper
MathWebSearch is an open-source, open-format, content-oriented search engine for mathematical formulae. It is a complete system capable of crawling, indexing, and querying expressions based on th...
Chapter and Conference Paper
We present an architecture and software framework for semantic allies: Semantic systems that complement existing software applications with semantic services and interactions based on a background ontology. On...
Chapter and Conference Paper
Successful representation and markup languages find a good balance between giving the user freedom of expression, enforcing the fundamental semantic invariants of the modeling framework, and allowing machine s...
Book
Chapter
In this appendix, we document the changes of the OMDoc format over the versions, provide quick reference tables, and discuss the validation helps.
Chapter
The OMDoc ( Open Mathematical Documents) format is a content markup scheme for (collections of) mathematical documents including articles, textbooks, interactive books, and courses. OMDoc also serves as the con...
Chapter
In this part we will address current applications, tools and projects using the OMDoc format. We will first discuss the possibilities and tools of processing documents in the OMDoc format via style sheets with th...
Chapter