{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216438},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_17","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"217-221","source":"Crossref","is-referenced-by-count":20,"title":["System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Franke","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"3","key":"17_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P. B. Andrews","year":"1996","unstructured":"Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321\u2013353, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. mega: Towards a mathematical assistant. InWilliam McCune, editor, Proceedings of the 14th Conference on Automated Deduction, number 1249 in LNAI, pages 252\u2013255, Townsville, Australia, 1997. Springer Verlag.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Christoph Benzm\u00fcller and Michael Kohlhase. LEO-a higher order theorem prover. In Claude Kirchner and H\u00e9l*#x00E8;ne Kirchner, editors, Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI, pages 139\u2013144, Lindau, Germany, 1998. Springer Verlag.","DOI":"10.1007\/BFb0054256"},{"key":"17_CR4","unstructured":"The open math standard. Open Math Consortium, http:\/\/www.openmath.org , 1998."},{"key":"17_CR5","unstructured":"T. Finin and R. Fritzson. KQML \u2014 a language and protocol for knowledge and information exchange. In Proceedings of the 13th Intl. Distributed Artificial Intelligence Workshop, pages 127\u2013136, Seattle, WA, USA, 1994."},{"key":"17_CR6","unstructured":"Andreas Franke, Stephan M. Hess, Christoph G. Jung, Michael Kohlhase, and Volker Sorge. Agent-oriented integration of distributed mathematical services. Journal of Universal Computer Science, 1999. forthcoming. 8 Either by using MathWeb directly, or by cooperating with the authors."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Xiaorong Huang and Armin Fiedler. Presenting machine-found proofs. In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th Conference on Automated Deduction, number 1104 in LNAI, pages 221\u2013225, New Brunswick, NJ, USA, 1996. Springer Verlag.","DOI":"10.1007\/3-540-61511-3_83"},{"issue":"3","key":"17_CR8","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1023\/A:1006059810729","volume":"21","author":"M. Kerber","year":"1998","unstructured":"Manfred Kerber, Michael Kohlhase, and Volker Sorge. Integrating computer algebra into proof planning. Journal of Automated Reasoning, 21(3):327\u2013355, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR9","unstructured":"Andreas Meier. Translation of automatically generated proofs at assertion level. Technical Report forthcoming, Universit\u00e4t des Saarlandes, 1999."},{"key":"17_CR10","unstructured":"J\u00f6rg Siekmann, Stephan Hess, Christoph Benzm\u00fcller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, and Volker Sorge. A distributed graphical user interface for the interactive proof system OMEGA. In Roland C. Backhouse, editor, User Interfaces for Theorem Provers, number 98-08 in Computing Science Reports, pages 130\u2013138, Department of Mathematics and Computing Science, Eindhoven Technical University, 1998."},{"key":"17_CR11","first-page":"13","volume-title":"6th CALCULEMUS and TYPES Workshop","author":"M. Kohlhase","year":"1998","unstructured":"M. Kohlhase, S. Hess, Ch. Jung and V. Sorge. An implementation of distributed mathematical services. In 6th CALCULEMUS and TYPES Workshop, Eindhoven, The Netherlands, July 13\u201315 1998. Electronic Procedings: http:\/\/www.win.tue.nl\/math\/dw\/pp\/calc\/proceedings.html ."},{"key":"17_CR12","unstructured":"Jon Siegel. CORBA: Fundamentals and Programming. John Wiley & Sons, Inc., 1996."},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Geoff Sutcliffe and Christian Suttner. The cade-14 atp system competition. Journal of Automated Reasoning, 21(2):177\u2013203, 1998.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:32Z","timestamp":1556960192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}