The categorial type of OpenMath objects

Abstract

We introduce a fundamental concept found in the formal semantics of language, categorial type logics, into the field of knowledge communication language design in general, and into mathematical content markup language design in particular. Categorial type logics permit the specification of type systems for knowledge communication languages that are both complete wrt. language structure and extensible wrt. the lexical component. We apply this concept to OpenMath, and propose a categorial type logic for that language which matches well with its intended semantics. The proposed type logic is a simpler version of the well-established L2 categorial type logic, from which it inherits decidability and other useful mathematical properties. As a practical result, we report a serious problem in the OpenMath 1.0 specification. © Springer-Verlag Berlin Heidelberg 2004.