Abstract
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.
Similar content being viewed by others
References
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: An approach. Kluwer Academic Publishers, Norwell (2000)
Bove, A., et al.: (2009) A brief overview of agda—a functional language with dependent types. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs’09) LNCS, vol. 5674, pp. 73–78 (2009)
Coq development team. The Coq Proof Assistant Reference Manual, version 8.4. Technical report (2012)
Nipkow, T., et al.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283, Springer, Berlin (2002)
Asperti, A., et al.: The Matita interactive theorem prover. In: 23rd International Conference on Automated Deduction (CADE’11), LNCS, vol. 6803, pp. 64–69 (2011)
Grabowski A., Kornilowicz A., Naumowicz A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153–245 (2010)
Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: 4th Conference on Interactive Theorem Proving (ITP’13), LNCS, vol. 7998, pp. 163–179 (2013)
Krebbers R., Spitters B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1), 1–27 (2013)
Hales, T.: The Flyspeck Project fact sheet. Project description. Available at http://code.google.com/p/flyspeck/ (2005)
Amorim, A., et al.: A verified information-flow architecture. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14) (2014)
Benton, N.: Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions? (2006)
Heras, J., Komendantskaya, E.: ML4PG: downloadable programs, manual, examples (2012–2014). http://staff.computing.dundee.ac.uk/katya/ML4PG/
Heras, J., Komendantskaya, E.: Proof Pattern Search in Coq/SSReflect (2014) http://arxiv.org/abs/1402.0081
Komendantskaya E. et al.: Machine learning for proof general: interfacing interfaces. Electron. Proc. Theor. Comput. Sci. 118, 15–41 (2013)
Aspinall, D.: Proof General: A generic tool for proof development. In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’00), LNCS, vol. 1785, pp. 38–43 (2000)
Bertot Y., Castéran P.: Interactive Theorem Proving and Program Development, Coq’Art: the Calculus of Constructions. Springer, Berlin (2004)
Gonthier G., Mahboubi A.: An introduction to small scale reflection. J. Formaliz. Reason. 3(2), 95–152 (2010)
Gonthier G.: Formal proof—the four-color theorem. Notices Am. Math. Soc. 55(11), 1382–1393 (2008)
Le Roux, S.: Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence. In: 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’07), LNCS, vol. 5674, pp. 293–309 (2009)
Vestergaard R.: A constructive approach to sequential nash equilibria. Inf. Process. Lett. 97, 46–51 (2006)
Moore, J S.: Models, Algebras and Logic of Engineering Software. In: Proving Theorems about Java and the JVM with ACL2, pp. 227–290. IOS Press, Amsterdam (2004)
Bundy A. et al.: AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Rep. 2(7), 1–29 (2012)
Johansson M. et al.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251–289 (2011)
Basin D. et al.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press, Cambridge (2005)
Kühlwein, D., et al.:Overview and evaluation of premise selection techniques for large theory mathematics. In: 6th International Joint Conference on Automated Reasoning (IJCAR’12), LNCS, vol. 7364, pp. 378–392 (2012)
Duncan, H.: The use of Data-Mining for the Automatic Formation of Tactics. PhD thesis, University of Edinburgh (2002)
Asperti, A., et al.: A content based mathematical search engine: Whelp. In: Post-Proceedings of the TYPES’04 International Conference, LNCS, vol. 3839, pp. 17–32 (2006)
Bishop C.: Pattern Recognition and Machine Learning. Springer, Berlin (2006)
Blum A.: Learning boolean functions in an infinite attribute space. Mach. Learn. 9(4), 373–386 (1992)
MATLAB.: version 7.14.0 (R2012a). The MathWorks Inc., Natick, Massachusetts (2012)
Hall M. et al.: The WEKA data mining software: an update. SIGKDD Explor. 11(1), 10–18 (2009)
Heras, J., et al.: roof-pattern recognition and lemma discovery in ACL2. In: 19th Logic for Programming Artificial Intelligence and Reasoning (LPAR-19), LNCS, vol. 8312, pp. 389–406 (2013)
Le Roux, S.: Acyclicity and finite linear extendability: a formal and constructive equivalence. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs’09), Emerging Trends Proceedings, pp. 154–169 (2007)
Lindholm, T., et al.: The Java Virtual Machine Specification: Java SE 7 edn. (2012)
Lange, C., et al.: A qualitative comparison of the suitability of four theorem provers for basic auction theory. In: Proceedings of Conferences on Intelligent Computer Mathematics (CICM’13), LNCS, vol. 7961, pp. 200–215 (2012)
Author information
Authors and Affiliations
Corresponding author
Additional information
The work was supported by EPSRC grant EP/J014222/1 and EP/K031864/1.
Rights and permissions
About this article
Cite this article
Heras, J., Komendantskaya, E. Recycling Proof Patterns in Coq: Case Studies. Math.Comput.Sci. 8, 99–116 (2014). https://doi.org/10.1007/s11786-014-0173-1
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11786-014-0173-1