{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:52Z","timestamp":1761610372960,"version":"build-2065373602"},"reference-count":27,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(05)80616-4","type":"journal-article","created":{"date-parts":[[2005,5,6]],"date-time":"2005-05-06T15:34:43Z","timestamp":1115393683000},"page":"469-480","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"title":["Integrating Computational and Deduction Systems Using OpenMath"],"prefix":"10.1016","volume":"23","author":[{"given":"O.","family":"Caprotti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.M.","family":"Cohen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80616-4_BIB1","unstructured":"The Lego Algebra Group. See http:\/\/www.cs.man.ac.uk\/~petera\/LAG\/."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB2","unstructured":"Iso 7-bit coded character set for information interchange. ISO 646:1983, 1983."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB3","doi-asserted-by":"crossref","unstructured":"John A. Abbott, Andr\u00e9 van Leeuwen, and A. Strotmann. OpenMath: Communicating Mathematical Information between Co-operating Agents in a Knowledge Network. Journal of Intelligent Systems, 1998. Special Issue: \u201cImproving the Design of Intelligent Systems: Outstanding Problems and Some Methods for their Solution.\u201d","DOI":"10.1515\/JISYS.1998.8.3-4.401"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB4","unstructured":"Anthony Bailey. The Machine-Checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester, January 15 January 15th 1998."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB5","series-title":"Proceedings of International Symposium on Symbolic and Algebraic Computation (ISSAC\u203295)","first-page":"150","article-title":"Theorems and Algorithms: An Interface between Isabelle and Maple","author":"Ballarin","year":"1995"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB6","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/jsco.1997.0171","article-title":"A Generic Approach to Building User Interfaces for Theorem Provers","volume":"25","author":"Bertot","year":"1998","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB7","doi-asserted-by":"crossref","unstructured":"B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, and D. Vasaru. A Survey of the Theorema Project. In Proceedings of ISSAC\u203297, Maui, Hawaii, July 1997. ACM.","DOI":"10.1145\/258726.258853"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB8","unstructured":"Stephen Buswell, Stan Devitt, Angel Diaz, Nico Poppelier, Bruce Smith, Neil Soiffer, Robert Sutor, and Stephen Watt. Mathematical Markup Language (MathML) 1.0 Specification. W3C Recommendation 19980407, April 1998. Available at http:\/\/www.w3.org\/TR\/REC-MathML\/."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB9","doi-asserted-by":"crossref","unstructured":"Piergiorgio Bertoliand Jacques Calmet, Fausto Giunchiglia, and Karsten Homann. Specification and Integration of Theorem Provers and Computer Algebra Systems. In J. Calmet and J. Plaza, editors, Artificial Intelligence and Symbolic Computation: International Conference AISC\u203298, volume 1476 of Lecture Notes in Artificial Intelligence, Plattsburgh, New York, USA, September 1998.","DOI":"10.1007\/BFb0055905"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB10","unstructured":"P. Chew, R. L. Constable, K. Pingali, S. Vavasis, and R. Zippel. Collaborative mathematics environments. Project Summary."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB11","series-title":"11th Conference on Automated Deduction volume 607 of Lecture Notes in Computer Science","first-page":"761","article-title":"Analytica - a theorem prover in Mathematica","author":"Clarke","year":"1992"},{"year":"1999","series-title":"Algebra Interactive, interactive course material, Number ISBN 3\ue4f8540\ue4f865368\ue4f86","author":"Cohen","key":"10.1016\/S1571-0661(05)80616-4_BIB12"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB13","unstructured":"OpenMath Consortium. The OpenMath Standard. OpenMath Deliverable 1.3.2a, February 1999. Available at http:\/\/www.nag.co.uk\/projects\/OpenMath.html."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB14","unstructured":"Projet Coq. The Coq Proof Assistant: The standard library, version 6.1 edition. Available at http:\/\/www.ens-lyon.fr\/LIP\/groupes\/coq."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB15","first-page":"241","author":"Dalmas","year":"1997","journal-title":"An OpenMath 1.0 Implementation"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB16","series-title":"ISSAC\u203298: International Symposium on Symbolic and Algebraic Computation","article-title":"Lightweight Formal Methods for Computer Algebra Systems","author":"Dunstan","year":"1998"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB17","series-title":"Software Agents","article-title":"Kqml as an agent communication language","author":"Finin","year":"1997"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB18","unstructured":"Foundation for Intelligent Physical Agents. The fipa \u203299 baselines. Available at http:\/\/www.fipa.org\/spec\/fipa99.html."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB19","unstructured":"A. Franke, S. Hess, Ch. Jung, M. Kohlhase, and V. Sorge. An implementation of distributed mathematical services. In Calculemus and Types 98, Eindhoven, July 1998."},{"issue":"3","key":"10.1016\/S1571-0661(05)80616-4_BIB20","first-page":"156","article-title":"Agent-Oriented Integration of Distributed Mathematical Services","volume":"5","author":"Franke","year":"1999","journal-title":"Journal of Universal Computer Science"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB21","series-title":"Logic Programming and Automated Reasoning: 4th International Conrerence volume 698 of Lecture Notes in Artificial Intelligence","first-page":"351","article-title":"Reasoning About the Reals: the marriage of HOL and Maple","author":"Harrison","year":"1993"},{"year":"1995","series-title":"Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Tr95-1509","author":"Jackson","key":"10.1016\/S1571-0661(05)80616-4_BIB22"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB23","unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, Edinburgh University, 1990."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB24","unstructured":"Z. Luo and P. Callaghan. Mathematical Vernacular and Conceptual Well-formedness in Mathematical Language. In Proceedings of the 2nd International Conference on Logical Aspects of Computational Linguistics 97, volume 1582 of Lecture Notes in Computer Science, Nancy, 1997."},{"year":"1992","series-title":"LEGO Proof Development System: User's Manual","author":"Luo","key":"10.1016\/S1571-0661(05)80616-4_BIB25"},{"key":"10.1016\/S1571-0661(05)80616-4_BIB26","unstructured":"L. Pottier and L. Th\u00e9ry. Certifier Computer Algebra. In Calculemus and Types \u203298, Eindhoven, July 1998. http:\/\/www-sop.inria.fr\/croap\/CFC\/."},{"key":"10.1016\/S1571-0661(05)80616-4_BIB27","unstructured":"PolyMath OpenMath Development Team. Java openmath library, version 0.5. Available at http:\/\/pdg.cecm.sfu.ca\/openmath\/lib\/, July 1998."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105806164?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105806164?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:17Z","timestamp":1761610097000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105806164"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066105806164"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80616-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Integrating Computational and Deduction Systems Using OpenMath","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80616-4","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1999 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}