Abstract
Complex automated proof strategies are often difficult to extract, visualise, modify, and debug. Traditional tactic languages, often based on stack-based goal propagation, make it easy to write proofs that obscure the flow of goals between tactics and are fragile to minor changes in input, proof structure or changes to tactics themselves. Here, we address this by introducing a graphical language called PSGraph for writing proof strategies. Strategies are constructed visually by “wiring together” collections of tactics and evaluated by propagating goal nodes through the diagram via graph rewriting. Tactic nodes can have many output wires, and use a filtering procedure based on goal-types (predicates describing the features of a goal) to decide where best to send newly-generated sub-goals. In addition to making the flow of goal information explicit, the graphical language can fulfil the role of many tacticals using visual idioms like branching, merging, and feedback loops. We argue that this language enables development of more robust proof strategies and provide several examples, along with a prototype implementation in Isabelle.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A., Ricciotti, W., Sacerdoti, C., Tassi, C.: A new type for tactics. In: PLMMS 2009, pp. 229–232 (2009)
Aspinall, D., Denney, E., Lüth, C.: A Tactic Language for Hiproofs. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC/Calculemus/MKM 2008. LNCS (LNAI), vol. 5144, pp. 339–354. Springer, Heidelberg (2008)
Autexier, S., Dietrich, D.: A Tactic Language for Declarative Proofs. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 99–114. Springer, Heidelberg (2010)
Bundy, A.: A science of reasoning. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 178–198 (1991)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press (2005)
Delahaye, D.: A Proof Dedicated Meta-Language. Electr. Notes Theor. Comput. Sci. 70(2), 96–109 (2002)
Dixon, L., Fleuriot, J.D.: IsaPlanner: A Prototype Proof Planner in Isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003)
Dixon, L., Kissinger, A.: Open Graphs and Monoidal Theories. CoRR, abs/1011.4114 (2010)
Giero, M., Wiedijk, F.: MMode, A Mizar Mode for the proof assistant Coq. Technical report (January 7, 2004)
Grov, G., Maclean, E.: Towards Automated Proof Strategy Generalisation. CoRR, abs/1303.2975 (2013)
Harrison, J.: A Mizar Mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 203–220. Springer, Heidelberg (1996)
Jamnik, M.: Mathematical Reasoning with Diagrams: From Intuition to Automation. CSLI Press, Stanford University (2001)
Kissinger, A., Merry, A., Dixon, L., Duncan, R., Soloviev, M., Frot, B.: Quantomatic (2011), https://sites.google.com/site/quantomatic/
Kissinger, A.: Pictures of Processes. PhD thesis, University of Oxford (2012)
Paulson, L.C.: Isabelle: The Next 700 Theorem Provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press (1990)
Selinger, P.: A Survey of Graphical Languages for Monoidal Categories. In: Coecke, B. (ed.) LFCS 1994. Lecture Notes in Physics, vol. 813, pp. 289–355. Springer, Heidelberg (2011)
Stampoulis, A., Shao, Z.: VeriML: Typed Computation of Logical Terms inside a Language with Effects. In: ICFP, pp. 333–344. ACM (2010)
Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards Formal Proof Script Refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS, vol. 6824, pp. 260–275. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grov, G., Kissinger, A., Lin, Y. (2013). A Graphical Language for Proof Strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)