{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T04:22:03Z","timestamp":1782879723610,"version":"3.54.5"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,3,10]],"date-time":"2010-03-10T00:00:00Z","timestamp":1268179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s11786-010-0025-6","type":"journal-article","created":{"date-parts":[[2010,3,9]],"date-time":"2010-03-09T02:30:48Z","timestamp":1268101848000},"page":"309-330","source":"Crossref","is-referenced-by-count":12,"title":["Tactics for Hierarchical Proof"],"prefix":"10.1007","volume":"3","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ewen","family":"Denney","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,3,10]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Aboul-Hosn, K.: A proof-theoretic approach to tactics. In: Borwein, J.M., Farmer, W.M. (eds.) Mathematical Knowledge Management, 5th International Conference, MKM 2006. Lecture Notes in Computer Science, vol. 4108, pp. 54\u201366. Springer, Berlin (2006)","DOI":"10.1007\/11812289_6"},{"issue":"4","key":"25_CR2","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1016\/j.jal.2005.10.005","volume":"4","author":"S.F. Allen","year":"2006","unstructured":"Allen S.F., Bickford M., Constable R.L., Eaton R., Kreitz C., Lorigo L., Moran E.: Innovations in computational type theory using Nuprl. J. Appl. Logic 4(4), 428\u2013469 (2006)","journal-title":"J. Appl. Logic"},{"key":"25_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0956796803004921","volume":"14","author":"A.W. Appel","year":"2004","unstructured":"Appel A.W., Felty A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14, 3\u201319 (2004)","journal-title":"J. Funct. Program."},{"issue":"2","key":"25_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti A., Coen C.S., Tassi E., Zacchiroli S.: User interaction with the matita proof assistant. J. Autom. Reason. 39(2), 109\u2013139 (2007)","journal-title":"J. Autom. Reason."},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof general: a generic tool for proof development. In: Graf, S., Schwartzbach, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785, pp. 38\u201342. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_3"},{"key":"25_CR6","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000, Reunion Island, France, November 6\u201310, 2000. Lecture Notes in Computer Science, vol. 1955, pp. 85\u201395 (2000)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: a hierarchical notion of proof tree. In: Proceedings of Mathematical Foundations of Programing Semantics (MFPS). Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, Amsterdam (2005)","DOI":"10.1016\/j.entcs.2005.11.063"},{"issue":"1","key":"25_CR8","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00881900","volume":"11","author":"A.P. Felty","year":"1993","unstructured":"Felty A.P.: Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reason. 11(1), 41\u201381 (1993)","journal-title":"J. Autom. Reason."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Howe, D.: Generalization and reuse of tactic proofs. In: Fifth International Conference on Logic Programming and Automated Reasoning LPAR. Lecture Notes in Computer Science, vol. 822. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58216-9_25"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, vol. 78, Springer, Berlin (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Proceeding of the IJCAR 2006, the Third International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 4130, pp. 177\u2013191. Springer, Berlin (2006)","DOI":"10.1007\/11814771_17"},{"key":"25_CR12","unstructured":"Heneveld, A.: Using features in interactive theorem proving. PhD thesis, School of Informatics, University of Edinburgh (2006)"},{"key":"25_CR13","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/j.entcs.2003.12.031","volume":"93","author":"G.I. Jojgov","year":"2004","unstructured":"Jojgov G.I., Geuvers H.: A calculus of tactics and its operational semantics. Electr. Notes Theor. Comput. Sci. 93, 118\u2013137 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR14","unstructured":"Kirchner, F.: Coq tacticals and PVS strategies: a small-step semantics. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, pp. 69\u201383. NASA\/CP-2003-212448 (2003)"},{"key":"25_CR15","unstructured":"Kirchner, F., Mu\u00f1oz, C.: pvs#: streamlined tacticals for PVS. In: Proceedings of STRATEGIES\u201906 (2006)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Kohlhase, M.: OMDoc\u2014an open markup format for mathematical documents. Lecture Notes in Computer Science, vol. 4180. Springer, Berlin (2006)","DOI":"10.1007\/11826095"},{"key":"25_CR17","unstructured":"Kolbe, T., Walther, C.: Reusing proofs. In: Cohn, A.G. (ed.) Proceedings of the Eleventh European Conference on Artificial Intelligence, pp. 80\u201384, Chichester, Wiley, New York (1994)"},{"key":"25_CR18","unstructured":"Kreitz, C.: The nuprl proof development system, version 5\u2014reference manual and user\u2019s guide. Department of Computer Science, Cornell-University, Ithaca 14853-7501 (2002)"},{"issue":"E","key":"25_CR19","first-page":"224","volume":"8","author":"A.P. Martin","year":"1996","unstructured":"Martin A.P., Gardiner P.H.B., Woodcock J.C.P.: A tactic calculus\u2014full version. Formal Aspects Comput. 8(E), 224\u2013285 (1996)","journal-title":"Formal Aspects Comput."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014a proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283, Springer, Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"25_CR21","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/s00165-003-0003-8","volume":"15","author":"M.V.M. Oliveira","year":"2003","unstructured":"Oliveira M.V.M., Cavalcanti A.L.C., Woodcock J.C.P.: ArcAngel: a tactic language for refinement. Formal Aspects Comput. 15(1), 28\u201347 (2003)","journal-title":"Formal Aspects Comput."},{"key":"25_CR22","first-page":"361","volume-title":"Logic and Computer Science","author":"L.C. Paulson","year":"1990","unstructured":"Paulson L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (eds) Logic and Computer Science, pp. 361\u2013386. Academic Press, London (1990)"},{"key":"25_CR23","first-page":"140","volume-title":"TYPES. Lecture Notes in Computer Science, vol. 996","author":"R. Pollack","year":"1994","unstructured":"Pollack R.: On extensibility of proof checkers. In: Dybjer, P., Nordstr\u00f6m, B., Smith, J.M. (eds) TYPES. Lecture Notes in Computer Science, vol. 996, pp. 140\u2013161. Springer, Berlin (1994)"},{"issue":"2","key":"25_CR24","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.entcs.2006.09.026","volume":"174","author":"C. Sacerdoti Coen","year":"2007","unstructured":"Sacerdoti Coen C., Tassi E., Zacchiroli S.: Tinycals: Step by step tacticals. Electr. Notes Theor. Comput. Sci. 174(2), 125\u2013142 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Schairer, A., Autexier, S., Hutter, D.: A pragmatic approach to reuse in tactical theorem proving. In: Proceedings of the 4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001). Electronic Notes in Computer Science, vol. 58, pp. 203\u2013216. Elsevier, Amsterdam (2001)","DOI":"10.1016\/S1571-0661(04)00286-5"},{"issue":"4","key":"25_CR26","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J. Siekmann","year":"2006","unstructured":"Siekmann J., Benzm\u00fcller C., Autexier S.: Computer supported mathematics with OMEGA. J. Appl. Logic 4(4), 533\u2013559 (2006)","journal-title":"J. Appl. Logic"},{"key":"25_CR27","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J. Siekmann","year":"1999","unstructured":"Siekmann J., Hess S., Benzm\u00fcller C., Cheikhrouhou L., Fiedler A., Horacek H., Kohlhase M., Konrad K., Meier A., Melis E., Pollet M., Sorge V.: LOUI: lovely omega user interface. Formal Aspects Comput. 11, 326\u2013342 (1999)","journal-title":"Formal Aspects Comput."},{"key":"25_CR28","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher-Order Logics. TPHOLs 2008 Lecture Notes in Computer Science, vol. 5170","author":"K. Slind","year":"2008","unstructured":"Slind K., Norrish M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds) Theorem Proving in Higher-Order Logics. TPHOLs 2008 Lecture Notes in Computer Science, vol. 5170, pp. 28\u201332. Springer, Berlin (2008)"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Wagner, M., Autexier, S., Benzm\u00fcller, C.: PLATO: A mediator between text-editors and proof assistance systems. In: Autexier, S., Benzm\u00fcller, C. (eds.) 7th Workshop on User Interfaces for Theorem Provers (UITP\u201906). Electronic Notes on Theoretical Computer Science, vol. 174(2), pp. 87\u2013107. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.09.024"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics TPHOLs\u201999. Lecture Notes in Computer Science, vol. 1690, pp. 167\u2013184. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48256-3_12"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-010-0025-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-010-0025-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-010-0025-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T18:32:27Z","timestamp":1559413947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-010-0025-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3,10]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["25"],"URL":"https:\/\/doi.org\/10.1007\/s11786-010-0025-6","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,3,10]]}}}