An Interactive Driver for Goal-directed Proof Strategies.pdf.pdf

Electronic Notes in puter Science 226 (2009) 89–105
ate/entcs
An Interactive Driver for Goal-directed Proof
Strategies
Andrea Asperti and Enrico Tassi
Department puter Science, University of Bologna
Mura Anteo Zamboni, 7 — 40127 Bologna, ITALY
******@ ******@
Abstract
Interactive Theorem Provers (ITPs) are tools meant to assist the user during the formal develop-
ment of mathematics. Automatic proof searching procedures are a desirable aid, and most ITPs
supply the user with an extensive set of facilities to improve automation. However, the black-box
nature of most automatic procedure conflicts with the interactive nature of these tools: a er
running an automatic procedure learns nothing by its execution (especially in case of failure), and
a trained user has no opportunities to interactively guide the procedure towards the solution, .
pruning wrong or not promising branches of the search tree. In this paper we discuss the imple-
mentation of the resolution based automatic procedure of the Matita ITP, explicitly conceived to
be interactively driven by the user through a suitable, simple graphical interface.
Keywords: Interactive theorem proving, SLD resolution, automation
1 Introduction
Most of the development effort behind Interactive Theorem Provers is devoted
to bridge the gap between the high level language used by humans for reason-
ing municating mathematics, and the low level foundational language
understood by ITPs. Among all facilities offered by ITPs, a high degree of
automation is certainly desirable and several works (see for example [12,11])
have been devoted to the integration of automatic proof search facilities in
interactive theorem provers. The machinery employed in this integration is
usually hidden to the user: when the automatic procedure finds a proof the
interactive theorem prover usually evaluates the trace left by the prover (if
any) and converts it, possibly using some reflection mecha