Presenting Proofs with Adapted Granularity

Marvin Schiller, Christoph Benzmüller

In: Bärbel Mertsching , Marcus Hund , Zaheer Aziz (editor). KI 2009: Advances in Artificial Intelligence. German Conference on Artificial Intelligence (KI-09) 32nd September 15-18 Paderborn Germany Pages 289-279 LNAI 5803 Springer Verlag 2009.


When mathematicians present proofs they usually adapt their explanations to their didactic goals and to the (assumed) knowledge of their addressees. Modern automated theorem provers, in contrast, present proofs usually at a fixed level of detail (also called granularity). Often these presentations are neither intended nor suitable for human use. A challenge therefore is to develop user- and goal-adaptive proof presentation techniques that obey common mathematical practice. We present a flexible and adaptive approach to proof presentation based on classification. Expert knowledge for the classification task can be handauthored or extracted from annotated proof examples via machine learning techniques. The obtained models are employed for the automated generation of further proofs at an adapted level of granularity.


Weitere Links

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz