User-adaptive proof explanation

Abstract

Today, automated theorem provers are becoming more and more important in practical industrial applications and more and more useful in mathematical education. For many applications, it is important that a deduction system communicates its proofs reasonably well to the human user. To this end, proof presentation systems have been developed. However, state-of-the-art proof presentation systems suffer from several deficiencies. First, they simply present the proofs, at best in a textbook-like format, without motivating why the proof is done as it is done. Second, they neglect the issue of user modeling and thus forgo the ability to adapt the presentation to the specific user, both with respect to the level of abstraction chosen for the presentation and with respect to steps that are trivial or easily inferable by the particular user and, therefore, should be omitted. Finally, they do not allow the user to interact with the system. He can neither inform the system that he has not understood some part of the proof, nor ask for a different explanation. Similarly, he cannot ask follow-up questions or questions about the background of the proof. As a first step to overcome these deficiencies, we shall develop in this talk a computational model of user-adaptive proof explanation, which is implemented in a generic, user-adaptive proof explanation system, called P.rex (for PRoof EXplainer). To do so, we shall use techniques from three different fields, namely from computational logic to represent proofs from various calculi with several levels of abstractions ensuring the correctness of the proofs; from cognitive science to model the users mathematical knowledge and skills; and from natural language processing to plan the explanation of the proofs and to accept and appropriately react to the user's interactions.

In jüngster Zeit werden automatische Beweissysteme für industrielle Zwecke immer wichtiger und im Mathematikunterricht zunehmend anwendbar. In vielen Anwendungen ist es wichtig, dass das Deduktionssystem seine Beweise dem menschlichen Benutzer in geeigneter Weise vermittelt. Daher werden spezielle Beweispräsentationssysteme entwickelt. Allerdings sind auch die modernsten Beweispräsentationssysteme in mehrfacher Hinsicht unzulänglich. Als ersten Schritt diese Problem zu beheben entwickeln wir in dieser Arbeit ein Berechnungsmodell für benutzeradaptive Beweiserklärung, die in dem generischen, benutzeradaptiven Beweiserklärungssytem P.rex implementiert ist. Dafür benutzen wir Techniken aus drei verschiedenen Gebieten, nämlich erstens aus der mathematischen Logik, um Beweise aus verschiedenen Kalkülen mit mehreren Abstraktionsebenen zu repräsentieren, wobei die Korrektheit der Beweise sichergestellt wird, zweitens aus der Kognitionswissenschaft, um das mathematische Wissen und die mathematischen Fertigkeiten des Benutzers zu modellieren, und drittens aus der Sprachverarbeitung, um die Beweiserklärung zu planen und um Benutzereingaben zu erlauben und auf sie geeignet zu reagieren.