Rating Disambiguation Errors

Andrea Asperti, Wilmer Ricciotti

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationCertified Programs and Proofs
Subtitle of host publicationSecond International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings
PublisherSpringer
Pages240-255
Number of pages16
ISBN (Electronic)978-3-642-35308-6
ISBN (Print)978-3-642-35307-9
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume7679
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Rating Disambiguation Errors'. Together they form a unique fingerprint.

Cite this