@InProceedings{	  PadovaniZacchiroli06,
  author	= {Luca Padovani and Stefano Zacchiroli},
  title		= {{F}rom {N}otation to {S}emantics: {T}here and {B}ack
		  {A}gain},
  booktitle	= {Proceedings of the 5th International Conference on
		  Mathematical Knowledge Management (MKM'06)},
  year		= {2006},
  volume	= {LNAI 4108},
  pages		= {194-207},
  publisher	= {Springer},
  url		= {http://www.di.unito.it/~padovani/Papers/lnai_4108.pdf},
  doi		= {10.1007/11812289\_16},
  abstract	= {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.}
}