Skip to main content
SpringerLink
Log in

TIP: Tools for Inductive Provers

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9450))

Included in the following conference series:

Abstract

TIP is a toolbox for users and developers of inductive provers. It consists of a large number of tools which can, for example, simplify an inductive problem, monomorphise it or find counterexamples to it. We are using TIP to help maintain a set of benchmarks for inductive theorem provers, where its main job is to encode aspects of the problem that are not natively supported by the respective provers. TIP makes it easier to write inductive provers, by supplying necessary tools such as lemma discovery which prover authors can simply import into their own prover.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

    Named after the lesser-known Ancient Greek philosopher.

References

  1. Amin, N., Leino, K.R.M., Rompf, T.: Computing with an SMT solver. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 20–35. Springer, Heidelberg (2014)

    Google Scholar 

  2. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard - version 2.5. http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf

  3. Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 493–507. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Barrett, C., de Moura, L. (eds.) SMT 2008: 6th International Workshop on Satisfiability Modulo. ACM International Conference Proceedings Series, vol. 367, pp. 1–5 (2008)

    Google Scholar 

  5. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: In Workshop on Intermediate Veri cation Languages, Boogie, August 2011

    Google Scholar 

  6. Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 87–102. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Chin, W.N., Darlington, J.: A higher-order removal method. LISP Symbolic Comput. 9(4), 287–322 (1996)

    Article  Google Scholar 

  8. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000 Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 268–279, ACM, New York (2000)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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, Heidelberg (2015)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Grechanik, S.A.: Proving properties of functional programs by equality saturation. Program. Comput. Softw. 41(3), 149–161 (2015)

    Article  MathSciNet  Google Scholar 

  13. 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, Heidelberg (2014)

    Google Scholar 

  14. Kaufmann, M., Panagiotis, M., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)

    Google Scholar 

  15. 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)

    Chapter  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)

    Google Scholar 

  17. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: The ACM Annual Conference, vol. 2 (1972)

    Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Wand, D., Weidenbach, C.: Automatic induction inside superposition. https://people.mpi-inf.mpg.de/~dwand/datasup/draft.pdf

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, Chalmers University of Technology, Gothenburg, Sweden

    Dan Rosén & Nicholas Smallbone

Authors
  1. Dan Rosén
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicholas Smallbone
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Dan Rosén or Nicholas Smallbone .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Appendices

A Rudimentocrates Source Code

figure h
figure i
figure j

B Example Run of Rudimentocrates

Here is an example showing the output of Rudimentocrates on a simple theory of append and reverse. The input file has a single conjecture that reverse (reverse xs) = xs:

figure k

Rudimentocrates first runs QuickSpec to discover likely lemmas about append and reverse:

figure l

It then goes into a proof loop, taking one conjecture at a time and trying to prove it. It prints :( when it failed to prove a conjecture, :) when it proved a conjecture without induction, and :D when it proves a conjecture with the help of induction:

figure m

Rudimentocrates prints a newline when it has tried all conjectures, then goes back and retries the failed ones (in case it can now prove them with the help of lemmas). In this case it manages to prove all the discovered conjectures, and prints out the following final theory. Notice that: (a) the property (= xs (reverse (reverse xs))) is now an axiom (assert) rather than a conjecture (assert-not), indicating that it has been proved, and (b) several other proved lemmas have been added to the theory file.

figure n

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rosén, D., Smallbone, N. (2015). TIP: Tools for Inductive Provers. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation