Abstract

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 wellformedness is purely extensional without an intuitive or formal condition that distinguishes well-formed objects from ill-formed ones. Moreover, some well-formed objects should arguably rather be ill-formed. We try to remedy that with a refined role system while preserving the simplicity of the existing one. In particular, by distinguishing syntactic and semantic roles, we can capture the intuitive notion of well-formedness better