{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:06Z","timestamp":1725471186197},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371045"},{"type":"electronic","value":"9783540371069"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11812289_9","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T08:23:44Z","timestamp":1159518224000},"page":"94-109","source":"Crossref","is-referenced-by-count":2,"title":["Synthesizing Proof Planning Methods and \u03a9-Ants Agents from Mathematical Knowledge"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominik","family":"Dietrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. Autexier","year":"2005","unstructured":"Autexier, S.: The CoRe calculus. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"9_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Benzm\u00fcller, Chr., Dietrich, D., Meier, A., Wirth, C.-P.: A generic modular data structure for proof attempts alternating on ideas and granularity. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, Springer, Heidelberg (2006)"},{"key":"9_CR3","volume-title":"The \u03bb-Calculus - Its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The \u03bb-Calculus - Its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"key":"9_CR4","unstructured":"Benzm\u00fcller, C., Sorge, V.: OANTS \u2013 an open approach at combining interactive and automated theorem proving. In: Kerber, M., Kohlhase, M. (eds.) Proceedings of Calculemus-2000, St. Andrews, UK, pp. 6\u20137. AK Peters (August 2001)"},{"key":"9_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/11542384_17","volume-title":"The Seventeen Provers of the World","author":"C. Benzm\u00fcller","year":"2006","unstructured":"Benzm\u00fcller, C., Fiedler, A., Meier, A., Pollet, M., Siekmann, J.: Omega. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, pp. 127\u2013141. Springer, Heidelberg (2006)"},{"key":"9_CR6","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.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 111\u2013120. Springer, Heidelberg (1988)"},{"key":"9_CR7","unstructured":"Dietrich, D.: The task-layer of the \u03a9mega system. Diploma thesis, FR 6.2 Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2006)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"E.W. Dijkstra","year":"1959","unstructured":"Dijkstra, E.W.: A note on two problems in connexion with graphs. Numerische Mathematik\u00a01, 269\u2013271 (1959)","journal-title":"Numerische Mathematik"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Farmer, W., Guttman, J., Thayer, F.J.: IMPS: An interactive mathematical proof system. Journal of Automated Reasoning\u00a011 (1993)","DOI":"10.1007\/BF00881906"},{"key":"9_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving \/","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. In: First-Order Logic and Automated Theorem Proving \/, 2nd edn., Springer, Heidelberg (1996)","edition":"2"},{"key":"9_CR11","unstructured":"Gentzen, G.: The Collected Papers of Gerhard Gentzen (1934-1938). In: Szabo, M.E. (ed.), North Holland, Amsterdam (1969)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF \u2013 A mechanised logic of computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"9_CR13","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"A. Meier","year":"2005","unstructured":"Meier, A., Melis, E.: Multi: A multi-strategy proof-planner. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"9_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054254","volume-title":"Automated Deduction - CADE-15","author":"J.D.C. Richardson","year":"1998","unstructured":"Richardson, J.D.C., Smaill, A., Green, I.M.: System description: proof planning in higher-order logic with \u03bb-clam. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, Springer, Heidelberg (1998)"},{"key":"9_CR15","unstructured":"Sorge, V.: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, FR 6.2 Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (November 2001)"},{"key":"9_CR16","unstructured":"Wack, B.: Typage et d\u00e9duction dans le calcul de r\u00e9\u00e9criture. Th\u00e8se de doctorat, Universit\u00e9 Henri Poincar\u00e9 (Nancy 1) (October 2005)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal proof sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11812289_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:05Z","timestamp":1619508425000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11812289_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371045","9783540371069"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11812289_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}