Publication
Presenting Proofs with Adapted Granularity
Marvin Schiller; Christoph Benzmüller
In: Bärbel Mertsching; Marcus Hund; Zaheer Aziz (Hrsg.). KI 2009: Advances in Artificial Intelligence. German Conference on Artificial Intelligence (KI-09), 32nd, September 15-18, Paderborn, Germany, Pages 289-279, LNAI, Vol. 5803, Springer Verlag, 2009.
Abstract
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.