{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:49Z","timestamp":1774837969434,"version":"3.50.1"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319630458","type":"print"},{"value":"9783319630465","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_32","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"528-545","source":"Crossref","is-referenced-by-count":9,"title":["A Proof Strategy Language and Proof Script Generation for Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Yutaka","family":"Nagashima","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"32_CR1","unstructured":"Blanchette, J., Fleury, M., Wand, D.: Concrete Semantics with Isabelle\/HOL (2015). http:\/\/people.mpi-inf.mpg.de\/~jblanche\/cswi\/"},{"issue":"1","key":"32_CR2","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016). http:\/\/dx.doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reasoning"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107\u2013121. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14203-1_9"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Breitner, J.: The safety of call arity. Archive of Formal Proofs, February 2015. http:\/\/isa-afp.org\/entries\/Call_Arity.shtml . Formal proof development","DOI":"10.1007\/978-3-319-14675-1_3"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111\u2013120. Springer, Heidelberg (1988). doi: 10.1007\/BFb0012826"},{"key":"32_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44404-1_7"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: A prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279\u2013283. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45085-6_22"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"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\u2013255. Springer, Heidelberg (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-21401-6_16","DOI":"10.1007\/978-3-319-21401-6_16"},{"key":"32_CR9","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"32_CR10","unstructured":"Lammich, P.: Collections framework. Archive of Formal Proofs, November 2009. http:\/\/isa-afp.org\/entries\/Collections.shtml . Formal proof development"},{"issue":"4","key":"32_CR11","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/BF01213535","volume":"8","author":"AP Martin","year":"1996","unstructured":"Martin, A.P., Gardiner, P.H.B., Woodcock, J.: A tactic calculus-abridged version. Formal. Asp. Comput. 8(4), 479\u2013489 (1996). http:\/\/dx.doi.org\/10.1007\/BF01213535","journal-title":"Formal. Asp. Comput."},{"key":"32_CR12","unstructured":"Martin, A., Gibbons, J.: A monadic interpretation of tactics (2002)"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-319-08970-6_25","volume-title":"Interactive Theorem Proving","author":"D Matichuk","year":"2014","unstructured":"Matichuk, D., Wenzel, M., Murray, T.: An isabelle proof method language. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 390\u2013405. Springer, Cham (2014). doi: 10.1007\/978-3-319-08970-6_25"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013388. Springer, Heidelberg (2015). http:\/\/dx.doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"32_CR15","unstructured":"Nagashima, Y.: Evaluation Results (2016). http:\/\/ts.data61.csiro.au\/Downloads\/cade26_results\/"},{"key":"32_CR16","unstructured":"Nagashima, Y.: Evaluation Tool (2016). http:\/\/ts.data61.csiro.au\/Downloads\/cade26_evaluation\/"},{"key":"32_CR17","unstructured":"Nagashima, Y.: Keep failed proof attempts in memory. In: Isabelle Workshop, Nancy, France, August 2016"},{"key":"32_CR18","unstructured":"Nagashima, Y.: PSL (2016). https:\/\/github.com\/data61\/PSL"},{"key":"32_CR19","unstructured":"Nagashima, Y., O\u2019Connor, L.: Close encounters of the higher kind - emulating constructor classes in standard ML, September 2016"},{"key":"32_CR20","unstructured":"Nipkow, T.: List index. Archive of Formal Proofs, February 2010. http:\/\/isa-afp.org\/entries\/List-Index.shtml . Formal proof development"},{"key":"32_CR21","unstructured":"Nipkow, T.: Skew heap. Archive of Formal Proofs, August 2014. http:\/\/isa-afp.org\/entries\/Skew_Heap.shtml . Formal proof development"},{"key":"32_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"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"},{"key":"32_CR23","unstructured":"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"},{"key":"32_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi: 10.1007\/3-540-55602-8_217"},{"key":"32_CR25","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. CoRR cs.LO\/9301105 (1993). http:\/\/arxiv.org\/abs\/cs.LO\/9301105"},{"key":"32_CR26","unstructured":"Sickert, S.: Linear temporal logic. Archive of Formal Proofs, March 2016. http:\/\/isa-afp.org\/entries\/LTL.shtml . Formal proof development"},{"key":"32_CR27","unstructured":"Sternagel, C.: Efficient mergesort. Archive of Formal Proofs, November 2011. http:\/\/isa-afp.org\/entries\/Efficient-Mergesort.shtml . Formal proof development"},{"key":"32_CR28","unstructured":"The Coq development team: The Coq proof assistant reference manual (2009)"},{"key":"32_CR29","unstructured":"Traytel, D.: A codatatype of formal languages. Archive of Formal Proofs, November 2013. http:\/\/isa-afp.org\/entries\/Coinductive_Languages.shtml . Formal proof development"},{"key":"32_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-15975-4_33","volume-title":"Functional Programming Languages and Computer Architecture","author":"P Wadler","year":"1985","unstructured":"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\u2013128. Springer, Heidelberg (1985). doi: 10.1007\/3-540-15975-4_33"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T18:04:35Z","timestamp":1659204275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}