{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:35Z","timestamp":1761611075754,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,12]]},"DOI":"10.1023\/a:1006059810729","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:38:24Z","timestamp":1040517504000},"page":"327-355","source":"Crossref","is-referenced-by-count":20,"title":["Integrating Computer Algebra into Proof Planning"],"prefix":"10.1007","volume":"21","author":[{"given":"Manfred","family":"Kerber","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"181208_CR1","series-title":"Technical Report","volume-title":"Objectives of OpenMath","author":"J. Abbot","year":"1996","unstructured":"Abbot, J., van Leeuwen, A., and Strotmann, A.: Objectives of OpenMath, Technical Report 12, RIACA, Eindhoven, June 1996."},{"key":"181208_CR2","doi-asserted-by":"crossref","unstructured":"Andrews, P. B.: Transforming matings into natural deduction proofs, in W. Bibel and R. Kowalski (eds), Proceedings of the 5th CADE, Les Arc, France, 1980, LNCS 87, Springer-Verlag, 1980, pp. 281\u2013292.","DOI":"10.1007\/3-540-10009-1_22"},{"key":"181208_CR3","doi-asserted-by":"crossref","unstructured":"Ballarin, C., Homann, K., and Calmet, J.: Theorems and algorithms: An interface between Isabelle and Maple, in A. H. M. Levelt (ed.), Proceedings of International Symposium on Symbolic and Algebraic Computation (ISSAC'95), ACM Press, 1995, pp. 150\u2013157.","DOI":"10.1145\/220346.220366"},{"key":"181208_CR4","unstructured":"Barendregt, H.: Computations and formal proofs in type theory, talk at the 2nd Meeting of the CALCULEMUS Project, Schlo\u03b2 Dagstuhl, Germany, 18.11.\u201320.11.1996. See also The quest for correctness, available as URL: ftp:\/\/ftp.cs.kun.nl\/pub\/CompMath.Found\/quest.ps.Z, 1996."},{"key":"181208_CR5","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Melis, E., Meier, A., Schaarschmidt, W., Siekmann, J., and Sorge, V.: \u03a9MEGA: Towards a mathematical assistant, in W. McCune (ed.), Proceedings of the 14th CADE, Townsville Australia, 1997, LNAI 1249, Springer-Verlag, 1997, pp. 252\u2013255.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"181208_CR6","unstructured":"Boyer, R. S. and Moore, J S.: Metafunctions, in R. S. Boyer and J S. Moore (eds), The Correctness Problem in Computer Science, Academic Press, 1981, pp. 103\u2013184."},{"key":"181208_CR7","first-page":"100","volume":"19","author":"B. Buchberger","year":"1996","unstructured":"Buchberger, B.: Mathematische Software-Systeme: Drastische Erweiterung des \u201cIntelligenzniveaus\u201d entsprechender Programme erwartet, Informatik Spektrum\n19\/2 (1996), 100\u2013101.","journal-title":"Informatik Spektrum"},{"key":"181208_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(85)80025-0","volume":"1","author":"B. Buchberger","year":"1985","unstructured":"Buchberger, B.: Symbolic computation (an editorial), J. Symbolic Comput.\n1 (1985), 1\u20136.","journal-title":"J. Symbolic Comput."},{"key":"181208_CR9","unstructured":"Buchberger, B.: Using Mathematica for doing simple mathematical proofs, invited talk at the 4th Tokyo Mathematica Users' Conference, November 2\u20133, 1996."},{"key":"181208_CR10","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs, in E. L. Lusk and R. A. Overbeek (eds), Proceedings of the 9th CADE, Argonne, Illinois, USA, 1988, LNCS 310, Springer-Verlag, 1988, pp. 111\u2013120.","DOI":"10.1007\/BFb0012826"},{"key":"181208_CR11","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., and Smaill, A.: Rippling: A heuristic for guiding inductive proofs, Artif. Intell.\n62 (1993), 185\u2013253.","journal-title":"Artif. Intell."},{"key":"181208_CR12","doi-asserted-by":"crossref","unstructured":"Char, B. W., Geddes, K. O., Gonnet, G. H., Leong, B. L., Monagan, M. B., and Watt, S. M.: First Leaves: A Tutorial Introduction to Maple V, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4615-6996-1"},{"key":"181208_CR13","volume-title":"Mechanical Geometry Theorem Proving, Mathematics and Its Applications","author":"S.-C. Chou","year":"1988","unstructured":"Chou, S.-C.: Mechanical Geometry Theorem Proving, Mathematics and Its Applications, D. Reidel Publishing Company, Dordrecht, 1988."},{"key":"181208_CR14","doi-asserted-by":"crossref","DOI":"10.1142\/2196","volume-title":"Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems","author":"S.-C. Chou","year":"1994","unstructured":"Chou, S.-C., Gao, X.-S., and Zhang, J.-Z.: Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, World Scientific, Singapore, 1994."},{"key":"181208_CR15","doi-asserted-by":"crossref","unstructured":"Clarke, E. and Zhao, X.: Analytica \u2013 A theorem prover in Mathematica, in Automated Deduction, 11th International Conference on Automated Deduction, Saratoga Springs, New York, 15\u201318 June 1992, pp. 761\u2013763.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"181208_CR16","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, D., Montagnac, F., and Prunet, V.: Integrated software components: A paradigm for control integration, in Proceedings of the European Symposium on Software Development Environments and CASE Technology, LNCS 509, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54194-2_35"},{"key":"181208_CR17","unstructured":"Constable, R. L. et al.: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"key":"181208_CR18","doi-asserted-by":"crossref","unstructured":"Fuchssteiner, B. et al. (The MuPAD Group): MuPAD User's Manual, Wiley, 1996.","DOI":"10.1007\/978-3-322-96649-0"},{"key":"181208_CR19","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Pecchiari, P., and Talcott, C.: Reasoning theories \u2013 towards an architecture for open mechanized reasoning systems, in F. Baader and K. U. Schulz (eds), Frontiers of Combining Systems (FroCoS-1): 1st International Workshop, Munich, Germany, 1996, Kluwer Acad. Publ., 1996, pp. 157\u2013174","DOI":"10.1007\/978-94-009-0349-4_8"},{"key":"181208_CR20","doi-asserted-by":"crossref","unstructured":"Harrison, J. and Th\u00e9ry, L.: Extending the HOL theorem prover with a computer algebra system to reason about the reals, in C.-J. H. Seger and J. J. Joyce (eds), Higher Order Logic Theorem Proving and its Applications (HUG'93), LNCS 780, Springer-Verlag, 1993, pp. 174\u2013184.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"181208_CR21","doi-asserted-by":"crossref","unstructured":"Harrison, J. and Th\u00e9ry, L.: Reasoning about the reals: The marriage of HOL and Maple, in A. Voronkov (ed.), Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93), St. Petersburg, Russia, LNAI 698, Springer-Verlag, 1993, pp. 351\u2013353.","DOI":"10.1007\/3-540-56944-8_68"},{"key":"181208_CR22","volume-title":"Reduce user's manual: Version 3.6","author":"A. C. Hearn","year":"1995","unstructured":"Hearn, A. C.: Reduce user's manual: Version 3.6, Technical Report, Rand Corporation, Santa Monica, CA, USA, 1995."},{"key":"181208_CR23","unstructured":"Homann, K. and Calmet, J.: An open environment for doing mathematics, in M. Wester, S. Steinberg, and M. Jahn (eds), Proceedings of 1st International IMACS Conference on Applications of Computer Algebra, Albuquerque, USA, 1995."},{"key":"181208_CR24","unstructured":"Howe, D. J.: Computational metatheory in Nuprl, in E. Lusk and R. Overbeek (eds), Proceedings of the 9th CADE, Argonne, Illinois, USA, 1988, LNCS 310, Springer-Verlag, 1988, pp. 238\u2013257."},{"key":"181208_CR25","doi-asserted-by":"crossref","unstructured":"Huang, X., Kerber, M., Kohlhase, M., Melis, E., Nesmith, D., Richts, J., and Siekmann, J.: \u03a9-MKRP: A proof development environment, in A. Bundy (ed.), Proceedings of the 12th CADE, Nancy, 1994, LNAI 814, Springer-Verlag, 1994, pp. 788\u2013792.","DOI":"10.1007\/3-540-58156-1_61"},{"key":"181208_CR26","doi-asserted-by":"crossref","unstructured":"Huang, X., Kerber, M., Kohlhase, M., and Richts, J.: Adapting methods to novel tasks in proof planning, in B. Nebel and L. Dreschler-Fischer (eds), KI-94: Advances in Artificial Intelligence \u2013 Proceedings of KI-94, 18th German Annual Conference on Artificial Intelligence, Saarbr\u00fccken, Germany, LNAI 861, Springer-Verlag, 1994, pp. 379\u2013380.","DOI":"10.1007\/3-540-58467-6_33"},{"key":"181208_CR27","doi-asserted-by":"crossref","unstructured":"Huang, X. and Fiedler, A.: Presenting machine-found proofs, in M. A. McRobbie and J. K. Slaney (eds), Proceedings of the 13th CADE, New Brunswick, NJ, USA, 1996, LNAI 1104, Springer-Verlag, 1996, pp. 221\u2013225.","DOI":"10.1007\/3-540-61511-3_83"},{"key":"181208_CR28","doi-asserted-by":"crossref","unstructured":"Jenks, R. D. and Sutor, R. S., AXIOM: The Scientific Computation System, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"181208_CR29","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0004-3702(88)90050-1","volume":"37","author":"D. Kapur","year":"1988","unstructured":"Kapur, D.: A refutational approach to theorem proving in geometry, Artif. Intell.\n37 (1988), 61\u201393.","journal-title":"Artif. Intell."},{"key":"181208_CR30","first-page":"595","volume":"7","author":"A. Karatsuba","year":"1963","unstructured":"Karatsuba, A. and Ofman, Y.: Multiplication of multidigit numbers by automata, Soviet Phys. Dokl.\n7 (1963), 595\u2013596.","journal-title":"Soviet Phys. Dokl."},{"key":"181208_CR31","first-page":"424","volume":"22","author":"R. Kowalski","year":"1979","unstructured":"Kowalski, R.: Algorithm = Logic + Control, Comm. Assoc. Comput. Machinery\n22 (1979), 424\u2013436.","journal-title":"Comm. Assoc. Comput. Machinery"},{"key":"181208_CR32","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.2172\/10129052","volume-title":"Otter 3.0 reference manual and guide","author":"W. W. McCune","year":"1994","unstructured":"McCune, W. W.: Otter 3.0 reference manual and guide, Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL, USA, 1994."},{"key":"181208_CR33","volume-title":"Diplomthemen SS-89","author":"Universit\u00e4t des Saarlandes","year":"1989","unstructured":"Universit\u00e4t des Saarlandes, Diplomthemen SS-89 Nr. 35, Fachschaft Wirtschaftswissenschaften, Saarbr\u00fccken, Germany, 1989."},{"key":"181208_CR34","volume-title":"The Mathematica Book: Version 3.0","author":"S. Wolfram","year":"1996","unstructured":"Wolfram, S.: The Mathematica Book: Version 3.0, 3rd edition, Wolfram Media, Inc., Champaign, IL, 1996.","edition":"3rd edition"},{"key":"181208_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-6639-0","volume-title":"Mechanical Theorem Proving in Geometries: Basic Principles, Texts and Monographs in Symbolic Computation","author":"W. Wu","year":"1994","unstructured":"Wu, W.: Mechanical Theorem Proving in Geometries: Basic Principles, Texts and Monographs in Symbolic Computation, Springer, Wien, 1994."},{"key":"181208_CR36","doi-asserted-by":"crossref","unstructured":"Zippel, R.: Effective Polynomial Computation, Kluwer Acad. Publ., 1993.","DOI":"10.1007\/978-1-4615-3188-3"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006059810729.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006059810729\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006059810729.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:33:02Z","timestamp":1749123182000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006059810729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,12]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,12]]}},"alternative-id":["181208"],"URL":"https:\/\/doi.org\/10.1023\/a:1006059810729","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,12]]}}}