Skip to main content
SpringerLink
Log in

Induction in Saturation-Based Proof Search

  • Conference paper
  • First Online:
Book cover Automated Deduction – CADE 27 (CADE 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11716))

Included in the following conference series:

Abstract

Many applications of theorem proving, for example program verification and analysis, require first-order reasoning with both quantifiers and theories such as arithmetic and datatypes. There is no complete procedure for reasoning in such theories but the state-of-the-art in automated theorem proving is still able to reason effectively with real-world problems from this rich domain. In this paper we contribute to a missing part of the puzzle: automated induction inside a saturation-based theorem prover. Our goal is to incorporate lightweight automated induction in a way that complements the saturation-based approach, allowing us to solve problems requiring a combination of first-order reasoning, theory reasoning, and inductive reasoning. We implement a number of techniques and heuristics and evaluate them within the Vampire theorem prover. Our results show that these new techniques enjoy practical success on real-world problems.

This work was supported by EPSRC Grant EP/P03408X/1. Andrei Voronkov was also partially supported by ERC Starting Grant 2014 SYMCAR 639270 and the Wallenberg Academy Fellowship 2014 – TheProSE.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    See https://github.com/vprover/vampire.

References

  1. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org

  2. Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392–406. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_27

    Chapter  Google Scholar 

  3. Comon, H.: Inductionless induction. In: Handbook of Automated Reasoning (in 2 vols.), pp. 913–962 (2001)

    Google Scholar 

  4. Cruanes, S.: Superposition with structural induction. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 172–188. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_10

    Chapter  Google Scholar 

  5. Dixon, L., Fleuriot, J.: Higher order rippling in IsaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 83–98. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30142-4_7

    Chapter  MATH  Google Scholar 

  6. Gupta, A., Kovács, L., Kragl, B., Voronkov, A.: Extensional crisis and proving identity. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 185–200. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_14

    Chapter  MATH  Google Scholar 

  7. Kaufmann, M., Strother Moore, J., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)

    Book  Google Scholar 

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

    Chapter  MATH  Google Scholar 

  9. Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. SIGPLAN Not. 52(1), 260–270 (2017)

    Article  Google Scholar 

  10. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  11. Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_21

    Chapter  Google Scholar 

  12. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 7, pp. 371–443. Elsevier Science (2001)

    Google Scholar 

  13. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning (in 2 vols.), pp. 335–367 (2001)

    Google Scholar 

  14. Reger, G., Bjørner, N., Suda, M., Voronkov, A.: AVATAR modulo theories. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016. EPiC Series in Computing, vol. 41, pp. 39–52. EasyChair (2016)

    Google Scholar 

  15. Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: 2nd Global Conference on Artificial Intelligence, GCAI 2016. EPiC Series in Computing, vol. 41, pp. 11–23. EasyChair (2016)

    Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-662-46081-8_5

    Chapter  Google Scholar 

  17. Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Trans. Comput. Logic 2(2), 155–181 (2001)

    Article  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  19. Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407–421. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_28

    Chapter  MATH  Google Scholar 

  20. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https://www.starexec.org

  21. Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)

    Article  Google Scholar 

  22. 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). https://doi.org/10.1007/978-3-319-08867-9_46

    Chapter  Google Scholar 

  23. Wand, D.: Superposition: types and induction. (Superposition: types et induction). Ph.D. thesis, Saarland University, Saarbrücken, Germany (2017)

    Google Scholar 

  24. Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, chap. 27, pp. 1965–2013. Elsevier Science (2001)

    Google Scholar 

Download references

Acknowledgements

We thank Andrew Reynolds for helping with obtaining CVC4 results.

Author information

Authors and Affiliations

  1. University of Manchester, Manchester, UK

    Giles Reger & Andrei Voronkov

  2. EasyChair, Manchester, UK

    Andrei Voronkov

Authors
  1. Giles Reger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Voronkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giles Reger .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Pascal Fontaine

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Reger, G., Voronkov, A. (2019). Induction in Saturation-Based Proof Search. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29436-6_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29435-9

  • Online ISBN: 978-3-030-29436-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation