Paper Info
Title
An Interactive Driver for Goal-directed Proof Strategies
Abstract
Interactive Theorem Provers (ITPs) are tools meant to assist the user during the formal development 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 newcomer 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, e.g. pruning wrong or not promising branches of the search tree. In this paper we discuss the implementation 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.
Year
DOI
Venue
2009
10.1016/j.entcs.2008.12.099
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
automation,automatic proof,black-box nature,interactive nature,goal-directed proof strategies,automatic procedure,sld resolution,interactive theorem provers,itps supply,matita itp,interactive theorem proving,interactive driver,trained user,desirable aid,automatic procedure conflict,theorem prover,procedural learning,graphical interface
Theorem provers,SLD resolution,Computer science,Formal development,Automation,Theoretical computer science,Graphical user interface,Proof assistant,Search tree
Journal
Volume
ISSN
Citations 
226,
Electronic Notes in Theoretical Computer Science
3
PageRank 
References 
Authors
0.45
15
2
Name
Order
Citations
PageRank
Andrea Asperti184975.19
Enrico Tassi232721.79