{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:05:46Z","timestamp":1737435946687,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540438656"},{"type":"electronic","value":"9783540454700"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45470-5_28","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:38:36Z","timestamp":1186900716000},"page":"319-331","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Inductive Theorem Proving and Computer Algebra in the MathWeb Software Bus"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Zimmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,21]]},"reference":[{"key":"28_CR1","unstructured":"A. Armando and D. Zini. Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture. In A. Poggi, editor, Proceedings of the AI*IA-TABOO Joint Workshop \u2018From Objects to Agents: Evolutionary Trends of Software Systems\u2019, Parma, Italy, May 2000."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"[BCF+97]_C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, K. Kohlhase, A. Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge.\u03a9mega: Towards a mathematical assistant. In W. McCune, editor, Proc. of the 14th Conference on Automated Deduction, volume 1249 of LNAI, pages 252\u2013255. Springer Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"issue":"3","key":"28_CR3","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1023\/A:1006079212546","volume":"21","author":"A. Bauer","year":"1998","unstructured":"A. Bauer, E. Clarke, and X. Zhao. Analytica \u2014 an Experiment in Combining Theorem Proving and Symbolic Computation. Journal of Automated Reasoning (JAR), 21(3):295\u2013325, 1998.","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"28_CR4","first-page":"185","volume":"62","author":"BSvH+93_A. Bundy","year":"1993","unstructured":"[BSvH+93]_A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. AI, 62:185\u2013253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.","journal-title":"AI"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. InM. E. Stickel, editor, Proc. of the 10th International Conference on Automated Deduction, pages 647\u2013648. Springer-Verlag, 1990. LNAI No. 449. Also available from Edinburgh as DAI Research Paper 507.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"28_CR6","unstructured":"O. Caprotti and A. M. Cohen. Draft of the Open Math standard. The Open Math Society, http:\/\/www.nag.co.uk\/proj ects\/OpenMath\/omstd\/ , 1998."},{"key":"28_CR7","unstructured":"The Mozart Consortium. The mozart programming system. http:\/\/www.mozart-oz.org\/ ."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"E. Clarke and X. Zhao. Analytica-A Theorem Prover for Mathematica. Technical Report CMU\/\/CS-92-117, Carnegie Mellon University, School of Computer Science, October 1992.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"28_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS-2000","author":"DCN+00_L. A. Dennis","year":"2000","unstructured":"[DCN+00]_L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The prosper toolkit. In Proc. of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS-2000, LNCS, Berlin, Germany, 2000. Springer Verlag."},{"key":"28_CR10","unstructured":"M. Dunstan, H. Gottliebsen, T. Kelsey, and U. Martin. A maple-pvs interface. Proc. of the Calculemus Symposium 2001, 2001."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"A. Franke and M. Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In Harald Ganzinger, editor, Proc. of the 16th Conference on Automated Deduction, volume 1632 of LNAI, pages 217\u2013221. Springer Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_17"},{"key":"28_CR12","series-title":"Lect Notes Comput Sci","first-page":"174","volume-title":"Higher Order Logic Theorem Proving and its Applications (HUG\u2019 93)","author":"J. Harrison","year":"1993","unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL Theorem Prover with a Computer Algebra System to Reason About the Reals. In C.-J. H. Seger J. J. Joyce, editor, Higher Order Logic Theorem Proving and its Applications (HUG\u2019 93), volume 780 of LNCS, pages 174\u2013184. Springer Verlag, 1993."},{"issue":"1-2","key":"28_CR13","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1996","unstructured":"A. Ireland and A. Bundy. Productive use of failure in inductive proof. JAR, 16(1-2):79\u2013111, 1996. Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.","journal-title":"JAR"},{"key":"28_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Design and Implementation of Symbolic Computation Systems; International Symposium, DISCO\u2019 96, Karlsruhe, Germany, September 18\u201320, 1996; Proc.","author":"M. Kerber","year":"1996","unstructured":"M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra with Proof Planning. In Jaques Calmet and Carla Limongelli, editors, Design and Implementation of Symbolic Computation Systems; International Symposium, DISCO\u2019 96, Karlsruhe, Germany, September 18\u201320, 1996; Proc., volume 1128 of LNCS. Springer Verlag, 1996."},{"key":"28_CR15","unstructured":"M. Kohlhase. OMDoc: An open markup format for mathematical documents. Seki Report SR-00-02, Fachbereich Informatik, Universit\u00e4t des Saarlandes, 2000. http:\/\/www.mathweb.org\/omdoc."},{"key":"28_CR16","unstructured":"E. Maclean, J. Fleuriot, and A. Smaill. Proof-planning non-standard analysis. In Proc. of the 7th International Symposium on Artificial Intelligence and Mathematics, 2002."},{"key":"28_CR17","unstructured":"J. Richardson and A. Smaill. Continuations of proof strategies. In Maria Paola Bonacina and Bernhard Gramlich, editors, Proc. of the 4th International Workshop on Strategies in Automated Deduction, Siena, Italy, June 2001."},{"key":"28_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/BFb0054254","volume-title":"Proc. of the 15th International Conference on Automated Deduction","author":"J.D.C. Richardson","year":"1998","unstructured":"J.D.C. Richardson, A. Smaill, and I. Green. System description: Proof planning in higher-order logic with lambda-clam. In C. Kirchner and H. Kirchner, editors, Proc. of the 15th International Conference on Automated Deduction, volume 1421 of LNCS, pages 129\u2013133. Springer-Verlag, 1998."},{"key":"28_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BFb0105418","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996","author":"A. Smaill","year":"1996","unstructured":"A. Smaill and I. Green. Higher-order annotated terms for proof search. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996, volume 1275 of LNCS, pages 399\u2013414, Turku, Finland, 1996. Springer-Verlag. Also available as DAI Research Paper 799."},{"key":"28_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BFb0015252","volume-title":"Computer Science Today","author":"G. Smolka","year":"1995","unstructured":"G. Smolka. The Oz programming model. In Jan van Leeuwen, editor, Computer Science Today, volume 1000 of LNCS, pages 324\u2013343. Springer-Verlag, Berlin, 1995."},{"key":"28_CR21","unstructured":"T. Walsh. Proof Planning in Maple. In Proc. of the CADE-17 workshop on Automated Deduction in the Context of Mathematics, 2000."},{"key":"28_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/3-540-55602-8_175","volume-title":"Proc. of the 11th Conference on Automated Deduction","author":"T. Walsh","year":"1992","unstructured":"T. Walsh, A. Nunes, and A. Bundy. The use of proof plans to sum series. In D. Kapur, editor, Proc. of the 11th Conference on Automated Deduction, volume 607 of LNCS, pages 325\u2013339, Saratoga Spings, NY, USA, 1992. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence, Automated Reasoning, and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45470-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:49:26Z","timestamp":1737362966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45470-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540438656","9783540454700"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-45470-5_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"21 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}