Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications
one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar,
comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully.
In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show
an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known
concepts and widely-used technologies and it can be easily adopted by other MKM applications.