{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:20:11Z","timestamp":1725488411285},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425250"},{"type":"electronic","value":"9783540447559"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44755-5_4","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T06:03:32Z","timestamp":1186725812000},"page":"27-42","source":"Crossref","is-referenced-by-count":15,"title":["Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Adams","sequence":"first","affiliation":[]},{"given":"Martin","family":"Dunstan","sequence":"additional","affiliation":[]},{"given":"Hanne","family":"Gottliebsen","sequence":"additional","affiliation":[]},{"given":"Tom","family":"Kelsey","sequence":"additional","affiliation":[]},{"given":"Ursula","family":"Martin","sequence":"additional","affiliation":[]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"4_CR1","unstructured":"Abbott, J., Van Leeuwen, A., AND Strotman, A. Objectives of OpenMath. Available from, Jan. 1995, http:\/\/www.rrz.uni-koeln.de\/themen\/Computeralgebra\/OpenMath\/ ."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Adams, A., Gottliebsen, H., Linton, S., AND Martin, U. Automated theorem proving in support of computer algebra: symbolic definite integration as a case study. In Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, Vancouver, Canada (1999), ACM Press.","DOI":"10.1145\/309831.309949"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Ballarin, C., Homann, K., AND Calmet, J. Theorems and algorithms: An interface between Isabelle and Maple. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (1995), A. Levelt, Ed., ACM Press, pp. 150\u2013157.","DOI":"10.1145\/220346.220366"},{"key":"4_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., AND Zhao, X. Analytica-an experiment in combining theorem proving and symbolic computation. Journal of Automated Reasoning 21 (1998), 295\u2013325.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055905","volume-title":"Artificial intelligence and symbolic computation","author":"P. Bertoli","year":"1998","unstructured":"Bertoli, P., Calmet, J., Guinchiglia, F., AND Homann, K. Specification and integration of theorem provers and computer algebra systems. In Artificial intelligence and symbolic computation (Plattsburgh, NY, 1998), no. 1476 in Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"4_CR6","unstructured":"Buchberger, B. Symbolic computation: Computer algebra and logic. In Frontiers of Combining Systems (1996), F. Baader and K. Schultz, Eds., Applied Logic Series, Kluwer Academic Publishers, pp. 193\u2013220."},{"key":"4_CR7","unstructured":"Buchberger, B. Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., AND Vasaru, D. A survey of the theorema project. In Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (1997), W. Kuechlin, Ed., ACM Press, pp. 384\u2013391."},{"key":"4_CR8","unstructured":"Calmet, J., AND Homann, K. Classification of communication and cooperation mechanisms for logical and symbolic computation systems. In Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany) (1996), F. Baader and K. U. Schulz, Eds., Applied Logic, Kluwer, pp. 221\u2013234."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Char, B. W.Maple V language Reference Manual. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4615-7386-9"},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"L. A. Dennis","year":"2000","unstructured":"Dennis, L. A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., AND Melham, T. The PROSPER Toolkit. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2000), vol. 1785 of Lecture Notes in Computer Science, Springer-Verlag."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dewar, M. Special Issue on OPENMATH. ACM SIGSAM Bulletin 34, 2 (June 2000).","DOI":"10.1145\/362001.362008"},{"issue":"2","key":"4_CR12","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., AND Sturm, T. REDLOG: Computer algebra meets computer logic. A CM SIGSAM Bulletin 31, 2 (June 1997), 2\u20139.","journal-title":"A CM SIGSAM Bulletin"},{"key":"4_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u2019 96","author":"B. Dutertre","year":"1996","unstructured":"Dutertre, B. Elements of mathematical analysis in PVS. In Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u2019 96 (Turku, Finland, Aug. 1996), J. von Wright, J. Grundy, and J. Harrison, Eds., vol. 1125 of Lecture Notes in Computer Science, Springer-Verlag, pp. 141\u2013156."},{"key":"4_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-44659-1_13","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"H. Gottliebsen","year":"2000","unstructured":"Gottliebsen, H. Transcendental Functions and Continuity Checking in PVS. In Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 (2000), J. Harrison and M. Aagaard, Eds., vol. 1869 of Lecture Notes in Computer Science, Springer-Verlag, pp. 198\u2013215."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Gray, S., Kajler, N., AND Wang, P. S. MP: A Protocol for Efficient Exchange of Mathematical Expressions. In Proc. of the International Symposium on Symbolic and Algebraic Computation (ISSAC\u201994), Oxford, GB (July 1994), M. Giesbrecht, Ed., ACM Press, pp. 330\u2013335.","DOI":"10.1145\/190347.190435"},{"key":"4_CR16","unstructured":"Harrison, J., AND Th\u00e9ry, L. Reasoning about the reals: the marriage of HOL and Maple. In Logic Programming and Automated Reasoning (1993), A. Voronkov, Ed., no. 698 in Lecture Notes in Artificial Intelligence, LPAR\u201993, Springer-Verlag, pp. 351\u2013359."},{"key":"4_CR17","series-title":"PhD thesis","volume-title":"Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra","author":"P. Jackson","year":"1995","unstructured":"Jackson, P.Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Apr. 1995."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Jenks, R. D., AND Sutor, R. S.AXIOM: the scientific computation system. Numerical Algorithms Group Ltd., 1992.","DOI":"10.1007\/978-1-4612-2940-7"},{"key":"4_CR19","unstructured":"Monagan, M., Geddes, K., Heal, K., Labahn, G., Vorkoetter, S., AND McCarron, J.Maple6 Programming Guide. Waterloo Maple Inc., 2000."},{"key":"4_CR20","unstructured":"Murphy, G. M.Ordinary differential equations and their solutions. D. van Nostrand Company, Inc., 1960."},{"key":"4_CR21","volume-title":"User Guide for the PVS Specification and Verification System","author":"S. Owre","year":"1993","unstructured":"Owre, S., Shankar, N., AND Rushby, J. M.User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"4_CR22","volume-title":"PVS Language Reference","author":"S. Owre","year":"1999","unstructured":"Owre, S., Shankar, N., Rushby, J. M., AND Stringer-Calvert, D. W. J.PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999."},{"key":"4_CR23","volume-title":"PVS System Guide","author":"S. Owre","year":"1999","unstructured":"Owre, S., Shankar, N., Rushby, J. M., AND Stringer-Calvert, D. W. J.PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999."},{"key":"4_CR24","unstructured":"Paulson, L. C.The Isabelle Reference Manual. Computer Laboratory, University of Cambridge, February 2001."},{"key":"4_CR25","unstructured":"Poll, E., AND Thompson, S. Adding the axioms to AXIOM: Towards a system of automated reasoning in Aldor. Tech. Rep. 6-98, Computing Laboratory, University of Kent at Canterbury, May 1998."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44755-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:10:34Z","timestamp":1556734234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44755-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425250","9783540447559"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-44755-5_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}