Abstract
Several approaches exist to data-mining big corpora of formal proofs. Some of these approaches are based on statistical machine learning, and some – on theory exploration. However, most are developed for either untyped or simply-typed theorem provers. In this paper, we present a method that combines statistical data mining and theory exploration in order to analyse and automate proofs in dependently typed language of Coq.
The work was supported by EPSRC grants EP/J014222/1 and EP/K031864/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Basin, D., et al.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press, New York (2005)
Bishop, C.: Pattern Recognition and Machine Learning. Springer, Heidelberg (2006)
Blanchette, J., et al.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016)
Coq development team. The Coq Proof Assistant Reference Manual, version 8.4pl3. Technical report (2013)
Czajka, L., Kaliszyk, C.: Goal translation for a Hammer for Coq. In: Proceeding of Hammers for Type Theories, EPTCS. vol. 210 , pp. 13-20 (2016)
Duncan, H.: The use of Data-Mining for the Automatic Formation of Tactics. Ph.D. thesis, University of Edinburgh (2002)
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection. J. Formalized Reasoning 3(2), 95–152 (2010)
Gransden, T., Walkinshaw, N., Raman, R.: Mining state-based models from proof corpora. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 282–297. Springer, Cham (2014). doi:10.1007/978-3-319-08434-3_21
Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: Search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 246–255. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_16
Hall, M., et al.: The WEKA data mining software: an update. SIGKDD Explor. 11(1), 10–18 (2009)
Heras, J., et al.: Computing persistent homology within Coq/SSReflect. ACM Trans. Comput. Logic 14(4), 26:1–26:16 (2013)
Heras, J., Komendantskaya, E.: Recycling proof patterns in Coq: case studies. J. Math. Comput. Sci. 8(1), 99–116 (2014)
Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 228–242. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_19
Heras, J., Komendantskaya, E., Johansson, M., Maclean, E.: Proof-pattern recognition and lemma discovery in ACL2. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 389–406. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_27
Johansson, M., et al.: Conjecture synthesis for inductive theories. J. Autom. Reasoning 47(3), 251–289 (2011)
Johansson, M., Rosén, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 108–122. Springer, Cham (2014). doi:10.1007/978-3-319-08434-3_9
Kaliszyk, C., Urban, J.: Lemma mining over HOL Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 503–517. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_34
Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109–128 (2015)
Kaufmann, M., Manolios, P., Moore, P. (eds.): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)
Komendantskaya, E., et al.: Machine learning for proof general: interfacing interfaces. Electron. Proc. Theor. Comput. Sci. 118, 15–41 (2013)
Kühlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35–50. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_6
The Univalent Foundations Program. Homotopy Type Theory. Institute for Advanced Study. https://github.com/HoTT/HoTT/wiki (2013)
Roux, S.: Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 293–309. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_21
Urban, J., et al.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning 50(2), 229–241 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Komendantskaya, E., Heras, J. (2017). Proof Mining with Dependent Types. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds) Intelligent Computer Mathematics. CICM 2017. Lecture Notes in Computer Science(), vol 10383. Springer, Cham. https://doi.org/10.1007/978-3-319-62075-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-62075-6_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-62074-9
Online ISBN: 978-3-319-62075-6
eBook Packages: Computer ScienceComputer Science (R0)