{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:14Z","timestamp":1725488954163},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_11","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"139-143","source":"Crossref","is-referenced-by-count":7,"title":["System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Zimmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"11_CR1","unstructured":"A. Armando, M. Kohlhase, and S. Ranise. Communication protocols for mathematical services based on KQML and OMRS. In Proc. of the Calculemus Symposium 2000), St. Andrews (Scotland), August 6\u20137, 2000."},{"key":"11_CR2","series-title":"PhD thesis","volume-title":"Automated Theory Formation in Pure Mathematics","author":"S. Colton","year":"2000","unstructured":"S. Colton. Automated Theory Formation in Pure Mathematics. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 2000."},{"key":"11_CR3","unstructured":"XML Remote Procedure Call Specification. http:\/\/www.xmlrpc.com\/ ."},{"key":"11_CR4","unstructured":"The mozart programming system. http:\/\/www.mozart-oz.org ."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"A. Franke and M. Kohlhase. System description: MathWeb, an agent-based communication layer for distributed automated theorem proving. In H. Ganzinger, ed., Proc. CADE-16, LNAI 1632, pp. 217\u2013221. Springer 1999.","DOI":"10.1007\/3-540-48660-7_17"},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-44659-1_13","volume-title":"Proc. of TPHOLs\u201900","author":"H. Gottliebsen","year":"2000","unstructured":"H. Gottliebsen. Transcendental Functions and Continuity Checking in PVS. In Proc. of TPHOLs\u201900, LNCS 1869, pp. 197\u2013214, Springer 2000."},{"key":"11_CR7","unstructured":"E. Melis. The \u2018Interactive Textbook\u2019 project. In D. McAllester, ed., Proc. of CADE WS \u201cDeduction and Education;\u201d, LNAI 1831. Springer Verlag, 2000."},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"ed.Proc. of CADE-11","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, ed.Proc. of CADE-11, LNCS 607, pp. 748\u2013752. Springer 1992."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"J. Siekmann, C. Benzm\u00fcller et al. Proof development with \u03c9mega. In A. Voronkov, ed., Proc. of CADE-18, LNAI Springer 2002.","DOI":"10.1007\/3-540-45620-1_12"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, ed., Proc. of CADE-12, LNAI 814, pp. 252\u2013266. Springer 1994.","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:56:20Z","timestamp":1556754980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}