Abstract
We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathers proof statistics and uses statistical pattern-recognition to pre-processes data from libraries, and then suggests auxiliary lemmas in new proofs by analogy with already seen examples. This paper presents the implementation of ACL2(ml) alongside theoretical descriptions of the proof-pattern recognition and lemma discovery methods involved in it.
The work was supported by EPSRC grants EP/J014222/11, EP/H024204/13 and a VINNMER Marie Curie Fellowship2.
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
Basin, D., Bundy, A., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press (2005)
Bishop, C.: Pattern Recognition and Machine Learning. Springer (2006)
Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. Journal of Applied Logic 4(4), 470–504 (2006)
Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392–406. Springer, Heidelberg (2013)
Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: Guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6–21. Springer, Heidelberg (2010)
Colton, S.: The HR Program for Theorem Generation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 285–289. Springer, Heidelberg (2002)
Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from previous proof experience: A survey. Technical report, Technische Universitat Munchen (1999)
Denzinger, J., Schulz, S.: Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts. Inform. and Comput. 162(1-2), 59–79 (2000)
Duncan, H.: The use of Data-Mining for the Automatic Formation of Tactics. PhD thesis, University of Edinburgh (2002)
Heras, J., et al.: ACL2(ml): downloadable programs, manual, examples (2013), http://staff.computing.dundee.ac.uk/jheras/acl2ml
Hetzl, S., Leitsch, A., Weller, D.: Towards algorithm cut-introduction. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 228–242. Springer, Heidelberg (2012)
Moore, J.: Proving theorems about Java and the JVM with ACL2. In: Models, Algebras and Logic of Engineering Software, pp. 227–290. IOS Press (2003)
Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. JAR 47(3), 251–289 (2011)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)
Kaufmann, M., Moore, J.S.: How to Prove Theorems Formally (2005), http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/main.ps
Kaufmann, M., Moore, J.S.: ACL2 version 6.2 (2013), http://www.cs.utexas.edu/users/moore/acl2/
Komendantskaya, E., Heras, J., Grov, G.: Machine Learning for Proof General: interfacing interfaces. ENTCS 118, 15–41 (2013)
Kühlwein, D., et al.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 378–392. Springer, Heidelberg (2012)
Martín-Mateos, F.J., et al.: ACL2 verification of simplicial degeneracy programs in the Kenzo system. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus/MKM 2009. LNCS (LNAI), vol. 5625, pp. 106–121. Springer, Heidelberg (2009)
McCasland, R.L., Bundy, A., Smith, P.F.: Ascertaining mathematical theorems. ENTCS 151(1), 21–38 (2006)
Montano-Rivas, O., et al.: Scheme-based theorem discovery and concept invention. Expert Syst. Appl. 39(2), 1637–1646 (2012)
Tsivtsivadze, E., Urban, J., Geuvers, H., Heskes, T.: Semantic graph kernels for automated reasoning. In: SDM 2011, pp. 795–803 (2011)
Urban, J., et al.: Malarea sg1- machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441–456. Springer, Heidelberg (2008)
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
Heras, J., Komendantskaya, E., Johansson, M., Maclean, E. (2013). Proof-Pattern Recognition and Lemma Discovery in ACL2. 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_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_27
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)