Software development for safety-critical or security systems cannot tolerate the risk of failure or malfunctioning. Formal methods provide mathematical techniques that are used for the specification, development and the verification of complex systems in order to increase their reliability and robustness. By now, there is a vast collection of formal specification languages, theorem provers and model checkers, which serve as development tools in formal methods. These are usually

We introduce the MMT language, which provides a simple and scalable Module system for the development of Mathematical Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation format that can represent the meta-theoretic foundations of mathematical and logical systems together with the represented knowledge itself and interlink the foundations at the meta-logical level. This ``logics-as-theories'' approach makes system behaviors as well as their represented knowledge interoperable and thus comparable.

Even though OpenMath has been around for more than 10 years, there is still confusion
about the ``semantics of OpenMath''. As the upcoming MathML 3 recommendation will
semantically base Content MathML on OpenMath Objects, this question becomes more
pressing.

One source of confusions about OpenMath semantics is that it is given on two levels: a
very weak algebraic semantics for expression trees, which is extended by considering
mathematical properties in content dictionaries that interpret the meaning of (constant)

OpenMath is a standard for the representation and communication of mathematical objects,
which are built up from symbols and variables using applications, binding expressions,
and key-value attributions. OpenMath2 introduced a set of symbol roles that can be
specified in content dictionaries to restrict the occurrences of the respective
symbols. This yields a simple, high-level notion of well-formed objects.

While this system is appealing in its simplicity, the definition of well-formedness is

We present a knowledge exchange format that is designed to support the exchange of
modularly structured information in mathematical and logical systems. This format
allows to encode mathematical knowledge in a logic-neutral representation format that
can represent the meta-theoretic foundations of the systems together with the knowledge itself
and to interlink the foundations at the meta-logical level. This ``logics-as-theories''
approach, makes system behaviors as well as their represented knowledge interoperable and

Logic is the study of formal languages for propositions and truth. Logics are used both as a foundation of mathematics and as specification languages in mathematics and computer science. Since logic is intricately intertwined with the nature of mathematics, the question how to represent logics in our minds is a constant challenge to our understanding. And only when it is understood can we begin to answer the corresponding question about logic translations. At the same time logics are used to a large extent in computer science to reason about both mathematics and software systems.

We propose extensions and corrections of the syntax and semantics of OMDoc that are necessary to define a formal semantics of OMDoc theory graphs. Since OMDoc theories are also OpenMath content dictionaries, this provides a module system and rudimentary syntax checking for OpenMath.

Our proposal includes a new constructor for OpenMath objects that is needed in the context of this module system. Together with related, so far unpublished work, this contribution provides a formal semantics and full type checking for OMDoc theory graphs.