Top

Published in:

2017 | OriginalPaper | Chapter

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

Authors : Yutaka Nagashima, Ramana Kumar

Published in: Automated Deduction – CADE 26

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

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.

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 Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints

next chapter The Binomial Pricing Model in Finance: A Formalization in Isabelle

Available only for authorised users

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.

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

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

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

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 CrossRef

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

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 CrossRef

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 CrossRef

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 CrossRef

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

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

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 CrossRefMATH

12.

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

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

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

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

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

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

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)

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 CrossRef

Title: A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Authors: Yutaka Nagashima
Ramana Kumar
Publisher: Springer International Publishing
Book: Automated Deduction – CADE 26
Print ISBN: 978-3-319-63045-8

Electronic ISBN: 978-3-319-63046-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63046-5_32

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