Argumentation in explanations to logical problems

Abstract

Explaining solutions to logical problems is one of the areas where argumentation in natural language plays a prominent role. One crucial reason for the difficulty in pursuing this issue in a systematic manner when relying on formal inference systems lies in the discrepancy between machine-oriented reasoning and human-adequate argumentation. Aiming at bridging these two divergent views, we present a model for producing human-adequate argumentation from machine-oriented inference structures. Ingredients of our method are techniques to build representations to suitable degrees of abstraction and explicitness, and a module for their interactive and adaptive exploration. The presented techniques are not only relevant for the interactive use of theorem provers, but they also have the potential to support the functionality of dialog-oriented tutorial systems.