Abstract / Description of output
Ambiguous notation is a powerful tool developed to deal with the complexity of mathematics without sacrificing clarity or conciseness. In the mechanized parsing of ambiguous terms, a disambiguation algorithm can be used to provide the system with the intelligence necessary to select valid interpretations for the overloaded symbols received in input.
Disambiguation works by means of an incremental analysis of the input term, progressively discarding all invalid interpretations. As a result, if the input term cannot be disambiguated, many errors will be produced, only a handful of which are truly meaningful to the user.
In this paper, we improve the existing technique to classify disambiguation errors by introducing a new heuristic to sort errors from the most meaningful to the least, showing that it can be implemented in a natural way in the existing disambiguation algorithm. We also describe a neat interface to present disambiguation errors to the user, suitable for the use in interactive theorem proving applications.
Disambiguation works by means of an incremental analysis of the input term, progressively discarding all invalid interpretations. As a result, if the input term cannot be disambiguated, many errors will be produced, only a handful of which are truly meaningful to the user.
In this paper, we improve the existing technique to classify disambiguation errors by introducing a new heuristic to sort errors from the most meaningful to the least, showing that it can be implemented in a natural way in the existing disambiguation algorithm. We also describe a neat interface to present disambiguation errors to the user, suitable for the use in interactive theorem proving applications.
Original language | English |
---|---|
Title of host publication | Certified Programs and Proofs |
Subtitle of host publication | Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings |
Publisher | Springer |
Pages | 240-255 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-642-35308-6 |
ISBN (Print) | 978-3-642-35307-9 |
DOIs | |
Publication status | Published - 2012 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Berlin Heidelberg |
Volume | 7679 |
ISSN (Print) | 0302-9743 |