Top

Published in:

2017 | Supplement | Chapter

Superposition with Structural Induction

Author : Simon Cruanes

Published in: Frontiers of Combining Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Superposition-based provers have been successfully used to discharge proof obligations stemming from proof assistants. However, many such obligations require induction to be proved. We present a new extension of typed superposition that can perform structural induction. Several inductive goals can be attempted within a single saturation loop, by leveraging \(\text {AVATAR}\) [1]. Lemmas obtained by generalization or theory exploration can be introduced during search, used, and proved, all in the same search space. We describe an implementation and present some promising results.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report

next chapter Subtropical Satisfiability

It might even induce rewriting loops in some cases where the term ordering used by superposition and the rewrite system are not compatible. In our experience this does not seem to happen often.

Our framework allows attempting to prove several distinct inductive goals to solve a single subgoal.

CVC4 1.5-prerelease r6317, see http://cvc4.cs.stanford.edu/web/ .

Commit 187b71af8d920d0634b2b8b34c4ac4834b2f6a94 at https://github.com/tip-org/benchmarks.

Experiments on TPTP were run on a 2.20 GHz Intel \(\text {Xeon}^\circledR \) CPU with 30 s timeout and a memory limit of 2 GB.

Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696–710. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_46

Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010, EasyChair (2012)

Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173–213 (2014)MathSciNetCrossRefMATH

Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111–126 (2002)MATH

Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 376–380. Springer, Heidelberg (2001). doi:10.1007/3-540-45744-5_29 CrossRef

Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System Description: Spass Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 514–520. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73595-3_38 CrossRef

Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 427–441. Springer, Heidelberg (1990). doi:10.1007/3-540-52885-7_105 CrossRef

Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 260–270. ACM (2017)

Kaufmann, M., Moore, J.S.: ACL2: an industrial strength version of Nqthm. In: Computer Assurance, COMPASS 1996, pp. 23–34. IEEE (1996)

10.

Biundo, S., Hummel, B., Hutter, D., Walther, C.: The karlsruhe induction theorem proving system. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 672–674. Springer, Heidelberg (1986). doi:10.1007/3-540-16780-3_132 CrossRef

11.

Stratulat, S.: A unified view of induction reasoning for first-order logic. In: Turing-100, The Alan Turing Centenary Conference (2012)

12.

Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_5

13.

Kersani, A., Peltier, N.: Combining superposition and induction: a practical realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 7–22. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40885-4_2 CrossRef

14.

Beeson, M.: Otter-lambda, a Theorem-prover with Untyped Lambda-unification. In: Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (2004)

15.

Wand, D., Weidenbach, C.: Automatic induction inside superposition (unpublished), April 2017. http://people.mpi-inf.mpg.de/dwand/datasup/d.pdf

16.

Riazanov, A., Voronkov, A.: Splitting without backtracking (2001)

17.

Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: TIP: tons of inductive problems. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 333–337. Springer, Cham (2015). doi:10.1007/978-3-319-20615-8_23 CrossRef

18.

Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62(2), 185–253 (1993)MathSciNetCrossRefMATH

19.

Boyer, R.S., Moore, J.S.: A Computational Logic Handbook: Formerly Notes and Reports in Computer Science and Applied Mathematics. Elsevier, San Diego (2014)

20.

Kapur, D., Subramaniam, M.: Lemma discovery in automating induction. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 538–552. Springer, Heidelberg (1996). doi:10.1007/3-540-61511-3_112

21.

Aubin, R.: Strategies for mechanizing structural induction. In: IJCAI (1977)

22.

Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31, 33–72 (2003)MathSciNetCrossRefMATH

23.

Burel, G.: Embedding deduction modulo into a prover. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 155–169. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15205-4_15 CrossRef

24.

Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). http://www.SMT-LIB.org

25.

Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 39–57. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_3 CrossRef

26.

Reynolds, A., Blanchette, J.C.: A decision procedure for (Co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 197–213. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_13 CrossRef

27.

Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisf. Boolean Model. Comput. 3, 21–46 (2007)MathSciNetMATH

28.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 CrossRef

29.

Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Trans. Comput. Log. (TOCL) 11(4), 27 (2010)MathSciNetMATH

30.

Zhang, H., Kapur, D., Krishnamoorthy, M.S.: A mechanizable induction principle for equational specifications. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 162–181. Springer, Heidelberg (1988). doi:10.1007/BFb0012831 CrossRef

31.

Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Hipspec: automating inductive proofs of program properties. In: ATx/WInG@ IJCAR (2012)

32.

Runciman, C., Naylor, M., Lindblad, F.: Smallcheck and lazy smallcheck: automatic exhaustive testing for small values. ACM Sigplan Not. 44, 37–48 (2008)CrossRef

33.

Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM Sigplan Not. 46(4), 53–64 (2011)CrossRef

34.

Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming, pp. 105–123, Citeseer (2007)

35.

Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique, September 2015

36.

Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 37–48. ACM (2016)

37.

Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefMATH

38.

Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47, 251–289 (2010)MathSciNetCrossRefMATH

Title: Superposition with Structural Induction
Author: Simon Cruanes
Publisher: Springer International Publishing
Book: Frontiers of Combining Systems
Print ISBN: 978-3-319-66166-7

Electronic ISBN: 978-3-319-66167-4

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-66167-4_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner