{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:32Z","timestamp":1725551912978},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540314301"},{"type":"electronic","value":"9783540314318"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11618027_9","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T06:48:07Z","timestamp":1137653287000},"page":"126-142","source":"Crossref","is-referenced-by-count":6,"title":["A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Dietrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Meier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claus-Peter","family":"Wirth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/10721959_11","volume-title":"Automated Deduction - CADE-17","author":"P.B. Andrews","year":"2000","unstructured":"Andrews, P.B., Bishop, M., Brown, C.E.: System description: TPS: A theorem proving system for type theory. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 164\u2013169. Springer, Heidelberg (2000)"},{"key":"9_CR2","volume-title":"International Journal on Software Tools for Technology Transfer, Special issue on Mechanized Theorem Proving for Technology","author":"S. Autexier","year":"1998","unstructured":"Autexier, S., Hutter, D., Langenstein, B., Mantel, H., Rock, G., Schairer, A., Stephan, W., Vogt, R., Wolpers, A.: VSE: Formal methods meet industrial needs. In: International Journal on Software Tools for Technology Transfer, Special issue on Mechanized Theorem Proving for Technology. Springer, Heidelberg (1998)"},{"key":"9_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-45085-6_29","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Avenhaus","year":"2003","unstructured":"Avenhaus, J., K\u00fchler, U., Schmidt-Samoa, T., Wirth, C.-P.: How to prove inductive theorems? QUODLIBET! In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 328\u2013333. Springer, Heidelberg (2003)"},{"key":"9_CR4","series-title":"Texts in Theoretical Computer Science, An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2014 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2014 Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, An EATCS Series. Springer, Heidelberg (2004)"},{"key":"9_CR5","unstructured":"Cheikhrouhou, L., Sorge, V.: PDS \u2014 A Three-Dimensional Data Structure for Proof Plans. In: Proc. of the Int. Conf. on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Applications, ACIDCA 2000 (2000)"},{"key":"9_CR6","unstructured":"Dixon, L.: Interactive and hierarchical tracing of techniques in IsaPlanner. In: Proc. of UITP 2005 (2005)"},{"key":"9_CR7","first-page":"1295","volume-title":"Proc. of the 17th International Joint Conference on Artificial Intelligence (IJCAI)","author":"A. Fiedler","year":"2001","unstructured":"Fiedler, A.: Dialog-driven adaptation of explanations of proofs. In: Proc. of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, WA, pp. 1295\u20131300. Morgan Kaufmann, San Francisco (2001)"},{"key":"9_CR8","unstructured":"The OMEGA Group: Proof development with \u03a9MEGA. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 143\u2013148. Springer, Heidelberg (2002)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"738","DOI":"10.1007\/3-540-58156-1_53","volume-title":"Automated Deduction - CADE-12","author":"X. Huang","year":"1994","unstructured":"Huang, X.: Reconstructing proofs at the assertion level. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 738\u2013752. Springer, Heidelberg (1994)"},{"issue":"C","key":"9_CR10","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.entcs.2004.02.021","volume":"103","author":"M. H\u00fcbner","year":"2004","unstructured":"H\u00fcbner, M., Autexier, S., Benzm\u00fcller, C., Meier, A.: Interactive theorem proving with tasks. Electronic Notes in Theoretical Computer Science\u00a0103(C), 161\u2013181 (2004)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Sengler, C.: INKA - The Next Generation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, Springer, Heidelberg (1996)"},{"key":"9_CR12","unstructured":"Kreitz, C., Lorigo, L., Eaton, R., Constable, R.L., Allen, S.F.: The nuprl open logical environment (2000)"},{"key":"9_CR13","unstructured":"Meier, A.: Proof Planning with Multiple Strategies. PhD thesis, Saarland Univ (2004)"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0004-3702(99)00076-4","volume":"115","author":"E. Melis","year":"1999","unstructured":"Melis, E., Siekmann, J.: Knowledge-Based Proof Planning. Artificial Intelligence\u00a0115(1), 65\u2013105 (1999)","journal-title":"Artificial Intelligence"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"9_CR16","first-page":"271","volume-title":"Proof Development in OMEGA: The Irrationality of Square Root of 2","author":"J. Siekmann","year":"2003","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof Development in OMEGA: The Irrationality of Square Root of 2, pp. 271\u2013314. Kluwer Academic Publishers, Dordrecht (2003)"},{"key":"9_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-36078-6_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Siekmann","year":"2002","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Pollet, M.: Proof development with OMEGA: Sqrt(2) is irrational. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 367\u2013387. Springer, Heidelberg (2002)"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C.-P. Wirth","year":"2004","unstructured":"Wirth, C.-P.: Descente infinie + Deduction. Logic J. of the IGPL\u00a012(1), 1\u201396 (2004)","journal-title":"Logic J. of the IGPL"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11618027_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T14:21:32Z","timestamp":1558275692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11618027_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314301","9783540314318"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11618027_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}