×

An interactive driver for goal-directed proof strategies. (English) Zbl 1291.68319

Autexier, Serge (ed.) et al., Proceedings of the 8th international workshop on user interfaces for theorem provers (UITP 2008), Montréal, Canada, August 22, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 226, 89-105 (2009).
Summary: 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.
For the entire collection see [Zbl 1280.68013].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Asperti, Andrea; Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano, A content based mathematical search engine: Whelp, (Post-proceedings of the Types 2004 International Conference. Post-proceedings of the Types 2004 International Conference, Lecture Notes in Computer Science, volume 3839 (2004), Springer-Verlag), 17-32 · Zbl 1172.68623
[2] Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, and Stefano Zacchiroli. Crafting a proof assistant. In Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK - April 18-21; Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, and Stefano Zacchiroli. Crafting a proof assistant. In Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK - April 18-21 · Zbl 1178.68524
[3] Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, and Stefano Zacchiroli. User interaction with the Matita proof assistant. Journal of Automated Reasoning; Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, and Stefano Zacchiroli. User interaction with the Matita proof assistant. Journal of Automated Reasoning · Zbl 1132.68673
[4] Andrea Asperti and Enrico Tassi. Higher order proof reconstruction from paramodulation-based refutations: The unit equality case. In Calculemus/MKM; Andrea Asperti and Enrico Tassi. Higher order proof reconstruction from paramodulation-based refutations: The unit equality case. In Calculemus/MKM · Zbl 1202.68370
[5] Barthe, Gilles; Ruys, Mark; Barendregt, Henk, A two-level approach towards lean proof-checking, (Types for Proofs and Programs. Types for Proofs and Programs, (Types 1995). Types for Proofs and Programs. Types for Proofs and Programs, (Types 1995), LNCS, volume 1158 (1995), Springer-Verlag), 16-35 · Zbl 1407.68431
[6] Boutin, Samuel, Using reflection to build efficient and certified decision procedures, (Abadi, Martin; Ito, Takahashi, Theoretical Aspect of Computer Software. Theoretical Aspect of Computer Software, TACS’97. Theoretical Aspect of Computer Software. Theoretical Aspect of Computer Software, TACS’97, Lecture Notes in Computer Science, volume 1281 (1997), Springer-Verlag), 515-529
[7] Christiane Bracchi, Christophe Gefflot, and Frederic Paulin. Combining propagation information and search tree visualization using ilog opl studio. In WLPE; Christiane Bracchi, Christophe Gefflot, and Frederic Paulin. Combining propagation information and search tree visualization using ilog opl studio. In WLPE
[8] Carro, M.; Hermenegildo, M. V., Tools for search tree visualization: the apt tool, (Deransart, P.; Hermenegildo, M. V.; Malusynsky, J., Analysis and Visualization tools for constraint programming, constraint debugging. Analysis and Visualization tools for constraint programming, constraint debugging, LNCS, volume 1870 (2000))
[9] Coquand, Thierry; Huet, Gérard P., The calculus of constructions, Inf. Comput., 76, 2/3, 95-120 (1988) · Zbl 0654.03045
[10] Fages, François; Soliman, Sylvain; Coolen, Rémi, CLPGUI: a generic graphical user interface for constraint logic programming, Journal of Constraints, 9, 4, 241-262 (October 2004), Special Issue on User-Interaction in Constraint Satisfaction
[11] Quigley, C.; Meng, J.; Paulson, L., Automation for interactive proof: First prototype, Information and Computation, 204, 10, 1575-1596 (2006) · Zbl 1103.68113
[12] J. Meng and L. Paulson. Experiments on supporting interactive proof using resolution. In David Basin and Michael Rusinowitch (editors), IJCAR; J. Meng and L. Paulson. Experiments on supporting interactive proof using resolution. In David Basin and Michael Rusinowitch (editors), IJCAR · Zbl 1126.68574
[13] Kowalski, Robert; Kuehner, Donald, Linear resolution with selection function, Artificial Intelligence, 2, 227-260 (1971) · Zbl 0234.68037
[14] Lloyd, John W., Foundations of Logic Programming (1987), Springer · Zbl 0668.68004
[15] César Muñoz. A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory; César Muñoz. A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory
[16] Christine Paulin-Mohring. Définitions Inductives en Théorie des Types d’Ordre Supŕieur; Christine Paulin-Mohring. Définitions Inductives en Théorie des Types d’Ordre Supŕieur
[17] Riazanov, Alexandre; Voronkov, Andrei, The design and implementation of vampire, AI Communications, 15, 2-3, 91-110 (2002) · Zbl 1021.68082
[18] Claudio Sacerdoti Coen. Mathematical Knowledge Management and Interactive Theorem Proving; Claudio Sacerdoti Coen. Mathematical Knowledge Management and Interactive Theorem Proving · Zbl 1108.68601
[19] Claudio Sacerdoti Coen and Enrico Tassi. Working with mathematical structures in type theory. In TYPES; Claudio Sacerdoti Coen and Enrico Tassi. Working with mathematical structures in type theory. In TYPES · Zbl 1138.68529
[20] Schulte, Christian, Oz Explorer: A visual constraint programming tool, (Naish, Lee, Proceedings of the Fourteenth International Conference on Logic Programming. Proceedings of the Fourteenth International Conference on Logic Programming, Leuven, Belgium (1997), The MIT Press: The MIT Press Cambridge, MA, USA), 286-300
[21] Simonis, H.; Aggoun, A., Search-tree visualization, (Deransart, P.; Hermenegildo, M. V.; Malusynsky, J., Analysis and Visualization tools for constraint programming, constraint debugging. Analysis and Visualization tools for constraint programming, constraint debugging, LNCS, volume 1870 (2000))
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.