{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:35Z","timestamp":1761611195670},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_9","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T14:36:30Z","timestamp":1167402990000},"page":"121-135","source":"Crossref","is-referenced-by-count":10,"title":["Non-trivial Symbolic Computations in Proof Planning"],"prefix":"10.1007","author":[{"given":"Volker","family":"Sorge","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/3-540-48660-7_8","volume-title":"Automated Deduction - CADE-16","author":"A. Adams","year":"1999","unstructured":"Adams, A., Gottliebsen, H., Linton, S., Martin, U.: VSDITLU: a verifiable symbolic definite integral table look-up. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 112\u2013126. Springer, Heidelberg (1999)"},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P. Andrews","year":"1996","unstructured":"Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A Theorem Proving System for Classical Type Theory. J. of Autom. Reasoning\u00a016(3), 321\u2013353 (1996)","journal-title":"J. of Autom. Reasoning"},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1145\/220346.220366","volume-title":"Proc. of ISSAC 1995","author":"C. Ballarin","year":"1995","unstructured":"Ballarin, C., Homann, K., Calmet, J.: Theorems and Algorithms: An Interface between Isabelle and Maple. In: Proc. of ISSAC 1995, pp. 150\u2013157. ACM Press, New York (1995)"},{"issue":"3","key":"9_CR4","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1023\/A:1006079212546","volume":"21","author":"A. Bauer","year":"1998","unstructured":"Bauer, A., Clarke, E., Zhao, X.: Analytica: an Experiment in Combining Theorem Proving and Symbolic Computation. J. of Autom. Reasoning\u00a021(3), 295\u2013325 (1998)","journal-title":"J. of Autom. Reasoning"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310. Springer, Heidelberg (1988)","DOI":"10.1007\/BFb0012826"},{"key":"9_CR6","volume-title":"Algebraic Programming with Magma","author":"J. Cannon","year":"1998","unstructured":"Cannon, J., Playoust, C.: Algebraic Programming with Magma. Springer, Heidelberg (1998)"},{"key":"9_CR7","unstructured":"Cheikhrouhou, L., Sorge, V.: PDS \u2014 A Three-Dimensional Data Structure for Proof Plans. In: Proc. of ACIDCA 2000 (2000)"},{"key":"9_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. J. of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"J. of Symbolic Logic"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, D., Montagnac, F., Prunet, V.: Integrated Software Components: a Paradigm for Control Integration. In: Endres, A., Weber, H. (eds.) SDE 1991. LNCS, vol.\u00a0509. Springer, Heidelberg (1991)","DOI":"10.1007\/3-540-54194-2_35"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R. Fikes","year":"1971","unstructured":"Fikes, R., Nilsson, N.: STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence\u00a02, 189\u2013208 (1971)","journal-title":"Artificial Intelligence"},{"key":"9_CR11","unstructured":"Franke, A., Hess, S.: Agent-Oriented Integration of Distributed Mathematical Services. J. of Universal Computer Science \u00a05(3), 156\u2013187 (1999)"},{"key":"9_CR12","unstructured":"The GAP Group: GAP \u2014 Groups, Algorithms, and Programming, Version 4, Aachen, St Andrews (1998), http:\/\/www-gap.dcs.st-and.ac.uk\/~gap"},{"key":"9_CR13","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das Logische Schlie\u03b2en I und II. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"key":"9_CR14","volume-title":"Introduction to HOL","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL. Cambridge Univ. Press, Cambridge (1993)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Edinburgh LCF","year":"1979","unstructured":"Gordon, M., Wadsworth, C.P., Milner, R. (eds.): Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"The \u03a9mega Group: \u03a9mega: Towards a Mathematical Assistant. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 252\u2013255. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63104-6_23"},{"issue":"3","key":"9_CR17","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A Skeptic\u2019s Approach to Combining HOL and Maple. J. of Autom. Reasoning\u00a021(3), 279\u2013294 (1998)","journal-title":"J. of Autom. Reasoning"},{"issue":"3","key":"9_CR18","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1023\/A:1006059810729","volume":"21","author":"M. Kerber","year":"1998","unstructured":"Kerber, M., Kohlhase, M., Sorge, V.: Integrating Computer Algebra Into Proof Planning. J. of Autom. Reasoning\u00a021(3), 327\u2013355 (1998)","journal-title":"J. of Autom. Reasoning"},{"key":"9_CR19","unstructured":"Melis, E.: The \u201cLimit\u201d Domain. In: Proc. of the Fourth International Conference on Artificial Intelligence in Planning Systems, pp. 199\u2013206 (1998)"},{"key":"9_CR20","unstructured":"Melis, E., Sorge, V.: Specialized External Reasoners in Proof Planning. Seki Report SR-00-01, Computer Science Department, Universit\u00e4t des Saarlandes (2000)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"9_CR22","volume-title":"The Maple Handbook: Maple V Release 5","author":"D. Redfern","year":"1998","unstructured":"Redfern, D.: The Maple Handbook: Maple V Release 5. Springer, Heidelberg (1998)"},{"key":"9_CR23","unstructured":"Sorge, V.: Integration eines Computeralgebrasystems in eine logische Beweisumgebung. Master\u2019s thesis, Universit\u00e4t des Saarlandes (November 1996)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:34:45Z","timestamp":1556019285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/10720084_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}