Interactive Theorem Proving with Tasks

Malte Hübner, Serge Autexier, Christoph Benzmüller, Andreas Meier

In: Electronic Notes in Theoretical Computer Science 103 C Pages 161-181 Elsevier 12/2004.


Interactive theorem proving systems for mathematics require user interfaces which can present proof states in a human understandable way. Often the underlying calculi of interactive theorem proving systems are problematic for comprehensible presentations since they are not optimally suited for practical, human oriented reasoning in mathematical domains. The recently developed CORE theorem proving framework (Autexier03) is an improvement of traditional calculi and facilitates flexible reasoning at the assertion level. We make use of COREs reasoning power and develop a communication layer on top of it, called the task layer. For this layer we define a set of manipulation rules that are implemented via COREs calculus rules. We thereby obtain a human oriented interaction layer that improves and combines ideas underlying the window inference technique (Robinson93), the proof by pointing approach (Bertot94), and the focus windows of Piroi02.


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