Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2017: Automated Deduction – CADE 26 pp 528–545Cite as

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL

  • Conference paper
  • First Online:

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

Abstract

We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL’s runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL’s monadic interpreter to show that the underlying idea of PSL is transferable to other ITPs.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    Constructor classes are a class mechanism on type constructors such as list and option, whereas type classes are a class mechanism on types such as int and double. Commonly used constructor classes include functor, applicative, monoid, and arrow.

  2. 2.

    In this sense, we implemented IDDFS as a tactic combinator.

References

  1. Blanchette, J., Fleury, M., Wand, D.: Concrete Semantics with Isabelle/HOL (2015). http://people.mpi-inf.mpg.de/~jblanche/cswi/

  2. Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101–148 (2016). http://dx.doi.org/10.6092/issn.1972-5787/4593

    MathSciNet  Google Scholar 

  3. Böhme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107–121. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_9

    Chapter  Google Scholar 

  4. Breitner, J.: The safety of call arity. Archive of Formal Proofs, February 2015. http://isa-afp.org/entries/Call_Arity.shtml. Formal proof development

  5. Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988). doi:10.1007/BFb0012826

    Chapter  Google Scholar 

  6. Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85–95. Springer, Heidelberg (2000). doi:10.1007/3-540-44404-1_7

    Chapter  Google Scholar 

  7. Dixon, L., Fleuriot, J.: IsaPlanner: A prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45085-6_22

    Chapter  Google Scholar 

  8. Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2003. LNCS, vol. 9195, pp. 246–255. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-319-21401-6_16

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

    Google Scholar 

  10. Lammich, P.: Collections framework. Archive of Formal Proofs, November 2009. http://isa-afp.org/entries/Collections.shtml. Formal proof development

  11. Martin, A.P., Gardiner, P.H.B., Woodcock, J.: A tactic calculus-abridged version. Formal. Asp. Comput. 8(4), 479–489 (1996). http://dx.doi.org/10.1007/BF01213535

    Article  MATH  Google Scholar 

  12. Martin, A., Gibbons, J.: A monadic interpretation of tactics (2002)

    Google Scholar 

  13. Matichuk, D., Wenzel, M., Murray, T.: An isabelle proof method language. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 390–405. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_25

    Google Scholar 

  14. de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2003. LNCS, vol. 9195, pp. 378–388. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-319-21401-6_26

  15. Nagashima, Y.: Evaluation Results (2016). http://ts.data61.csiro.au/Downloads/cade26_results/

  16. Nagashima, Y.: Evaluation Tool (2016). http://ts.data61.csiro.au/Downloads/cade26_evaluation/

  17. Nagashima, Y.: Keep failed proof attempts in memory. In: Isabelle Workshop, Nancy, France, August 2016

    Google Scholar 

  18. Nagashima, Y.: PSL (2016). https://github.com/data61/PSL

  19. Nagashima, Y., O’Connor, L.: Close encounters of the higher kind - emulating constructor classes in standard ML, September 2016

    Google Scholar 

  20. Nipkow, T.: List index. Archive of Formal Proofs, February 2010. http://isa-afp.org/entries/List-Index.shtml. Formal proof development

  21. Nipkow, T.: Skew heap. Archive of Formal Proofs, August 2014. http://isa-afp.org/entries/Skew_Heap.shtml. Formal proof development

  22. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). http://dx.doi.org/10.1007/3-540-45949-9

    MATH  Google Scholar 

  23. Nishihara, T., Minamide, Y.: Depth first search. Archive of Formal Proofs, June 2004. http://isa-afp.org/entries/Depth-First-Search.shtml. Formal proof development

  24. Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). doi:10.1007/3-540-55602-8_217

    Google Scholar 

  25. Paulson, L.C.: The foundation of a generic theorem prover. CoRR cs.LO/9301105 (1993). http://arxiv.org/abs/cs.LO/9301105

  26. Sickert, S.: Linear temporal logic. Archive of Formal Proofs, March 2016. http://isa-afp.org/entries/LTL.shtml. Formal proof development

  27. Sternagel, C.: Efficient mergesort. Archive of Formal Proofs, November 2011. http://isa-afp.org/entries/Efficient-Mergesort.shtml. Formal proof development

  28. The Coq development team: The Coq proof assistant reference manual (2009)

    Google Scholar 

  29. Traytel, D.: A codatatype of formal languages. Archive of Formal Proofs, November 2013. http://isa-afp.org/entries/Coinductive_Languages.shtml. Formal proof development

  30. Wadler, P.: How to replace failure by a list of successes a method for exception handling, backtracking, and pattern matching in lazy functional languages. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 113–128. Springer, Heidelberg (1985). doi:10.1007/3-540-15975-4_33

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank Jasmin C. Blanchette for his extensive comments that improved the evaluation of try_hard. Pang Luo helped us for the evaluation. Leonardo de Moura, Daniel Matichuk, Kai Engelhardt, and Gerwin Klein provided valuable comments on an early draft of this paper. We thank the anonymous reviewers for useful feedback, both at CADE-26 and for previous versions of this paper at other conferences. This work was partially funded by the ERC Consolidator grant 649043 - AI4REASON.

Author information

Authors and Affiliations

  1. Data61, CSIRO, Sydney, Australia

    Yutaka Nagashima & Ramana Kumar

  2. Data61, CSIRO/UNSW, Sydney, Australia

    Ramana Kumar

Authors
  1. Yutaka Nagashima
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ramana Kumar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ramana Kumar .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

A Appendix: Details of the Evaluation

A Appendix: Details of the Evaluation

All evaluations were conducted on a Linux machine with Intel (R) Core (TM) i7-600 @ 3.40 GHz and 32 GB memory. For both tools, we set the time-out of proof search to 30 and 300 s for each proof obligation.

Prior to the evaluation, the relevance filter of sledgehammer was trained on 27,041 facts and 18,695 non-trivial Isar proofs from the background libraries imported by theories under evaluation for both tools. Furthermore, we forbid sledgehammer inside PSL from using the smt method for proof reconstruction, since the AFP does not permit this method.

Note that try_hard does not use parallel strategy combinators which exploit parallelism. The evaluation tool does not allow try_hard to use multiple threads either. Therefore, given the same time-out, try_hard and sledgehammer enjoy the same amount of computational resources, assuring the fairness of the evaluation results.

The evaluation tool [16] and results [15] are available at our websites. We provide the evaluation tool and results in the following websites:

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Nagashima, Y., Kumar, R. (2017). A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation