The disambiguation approach to the input of formulae enables users of mathematical assistants to type correct formulae in
a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae however, far too many
typing errors are generated; among them we want to present only errors related to the formula interpretation meant by the
user, hiding errors related to other interpretations.
We study disambiguation errors and how to classify them into the spurious and genuine error classes. To this end we give a
general presentation of the classes of disambiguation algorithms and efficient disambiguation algorithms. We also quantitatively
assess the quality of the presented error classification criteria benchmarking them in the setting of a formal development
of constructive algebra.
Mathematics Subject Classification (2000). Primary 68T99 - Secondary 03B70
Keywords. Ambiguity - semantic analysis - user interaction - metavariables
Partially supported by the Strategic Project “DAMA: Dimostrazione Assistita per la Matematica e l’Apprendimento” of the University
of Bologna.