{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:58:07Z","timestamp":1725487087574},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426127"},{"type":"electronic","value":"9783540454229"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45422-5_29","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T15:01:34Z","timestamp":1183561294000},"page":"409-424","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Experiments with an Agent-Oriented Reasoning System"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Manfred","family":"Kerber","sequence":"additional","affiliation":[]},{"given":"Mateja","family":"Jamnik","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,9,3]]},"reference":[{"key":"29_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of RTA-95","author":"J. Avenhaus","year":"1995","unstructured":"J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT:A system for distributed equational deduction. In Proc. of RTA-95, LNCS 914. Springer, 1995."},{"issue":"2","key":"29_CR2","doi-asserted-by":"publisher","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"P. Andrews","year":"1972","unstructured":"P. Andrews. General models, descriptions and choice in type theory. Journal of Symbolic Logic, 37(2):385\u2013394, 1972.","journal-title":"Journal of Symbolic Logic"},{"key":"29_CR3","unstructured":"A. Armando and D. Zini. nterfacing computer algebra and deduction systems via the logic broker architecture. In [CAL01]."},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller et al. Omega: Towards a mathematical assistant. In Proc. of CADE-14, LNAI 1249. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_23"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller, M. Jamnik, M. Kerber, and V. Sorge. Agent Based Mathematical Reasoning. In CALCULEMUS-99, Systems for Integrated Computation and Deduction, volume 23 (3) of ENTCS. Elsevier, 1999.","DOI":"10.1016\/S1571-0661(05)82522-8"},{"key":"29_CR6","unstructured":"C. Benzm\u00fcller and M. Kohlhase. LEO-a higher-order theorem prover. In Proc. of CADE-15, LNAI 1421. Springer, 1998."},{"key":"29_CR7","unstructured":"M. Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, in press, 2001."},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"C. Benzm\u00fcller and V. Sorge. Critical Agents Supporting Interactive Theorem Proving. Proc. of EPIA-99, LNAI 1695, Springer, 1999.","DOI":"10.1007\/3-540-48159-1_15"},{"key":"29_CR9","unstructured":"C. Benzm\u00fcller and V. Sorge. OANTS-An open approach at combining Interactive and Automated Theorem Proving. In [CAL01]."},{"key":"29_CR10","unstructured":"CALCULEMUS-2000, Systems for Integrated Computation and Deduction. AK Peters, 2001."},{"key":"29_CR11","unstructured":"L. Cheikhrouhou and V. Sorge. PDS A Three-Dimensional Data Structure for Proof Plans. In Proc. of ACIDCA\u20192000, 2000."},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"I. Dahn and J. Denzinger. Cooperating theorem provers. In Automated Deduction-A Basis for Applications, volume II. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_14"},{"key":"29_CR13","unstructured":"J. Denzinger and D. Fuchs. Cooperation of Heterogeneous Provers. In Proc. of IJCAI-99, 1999."},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"J. Denzinger and M. Kronenburg. Planning for distributed theorem proving: The teamwork approach. In Proc. of KI-96, LNAI 1137. Springer, 1996.","DOI":"10.1007\/3-540-61708-6_45"},{"issue":"3","key":"29_CR15","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"A. Franke, S. Hess, Ch. Jung, M. Kohlhase, and V. Sorge. Agent-Oriented Integration of Distributed Mathematical Services. Journal of Universal Computer Science, 5(3):156\u2013187, 1999.","journal-title":"Journal of Universal Computer Science"},{"key":"29_CR16","unstructured":"M. Fisher and A. Ireland. Multi-agent proof-planning. CADE-15Workshop \u201cUsing AI methods in Deduction\u201d, 1998."},{"key":"29_CR17","unstructured":"A. Fiedler. P.rex: An interactive proof explainer. In R. Gor\u00e9, A. Leitsch, and T. Nipkow (eds), Automated Reasoning-Proceedings of the First International Joint Conference, IJCAR, LNAI 2083. Springer, 2001."},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"M. Fisher. An Open Approach to Concurrent Theorem Proving. In Parallel Processing for Artificial Intelligence, volume 3. Elsevier, 1997.","DOI":"10.1016\/S0923-0459(97)80011-0"},{"key":"29_CR19","unstructured":"M. Fisher and M. Wooldridge. A Logical Approach to the Representation of Societies of Agents. In Artificial Societies. UCL Press, 1995."},{"issue":"1-2","key":"29_CR20","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF00244460","volume":"16","author":"A. Ireland","year":"1995","unstructured":"A. Ireland and A. Bundy. Productive use of failure in inductive proof. Special Issue of the Journal of Automated Reasoning, 16(1-2):79\u2013111, 1995.","journal-title":"Special Issue of the Journal of Automated Reasoning"},{"key":"29_CR21","doi-asserted-by":"crossref","unstructured":"A. Meier. Tramp-transformation of machine-found proofs into ND-proofs at the assertion level. In Proc. of CADE-17, LNAI 1831. Springer, 2000.","DOI":"10.1007\/10721959_37"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"J. M\u00fcller. A Cooperation Model for Autonomous Agents. In Proc. of the ECAI\u201996 Workshop Intelligent Agents III, LNAI 1193. Springer, 1997.","DOI":"10.1007\/BFb0013590"},{"issue":"2","key":"29_CR23","first-page":"23","volume":"3","author":"H. Nii","year":"1982","unstructured":"H. Nii, E. Feigenbaum, J. Anton, and A. Rockmore. Signal-to-symbol transformation: HASP\/SIAP case study. AIMagazine, 3(2):23\u201335, 1982.","journal-title":"AIMagazine"},{"key":"29_CR24","unstructured":"J. Rice. The ELINT Application on Poligon: The Architecture and Performance of a Concurrent Blackboard System. In Proc. of IJCAI-89. Morgan Kaufmann, 1989."},{"issue":"3","key":"29_CR25","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/s001650050053","volume":"11","author":"J. Siekmann","year":"1999","unstructured":"J. Siekmann et al. Loui: Lovely Omega user interface. Formal Aspects of Computing, 11(3):326\u2013342, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"29_CR26","unstructured":"G. Weiss, editor. Multiagent systems: a modern approach to distributed artificial intelligence. MIT Press, 1999."},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"A. Wolf. P-SETHEO: Strategy Parallelism in Automated Theorem Proving. In Proc. of TABLEAUX-98, LNAI 1397. Springer, 1998.","DOI":"10.1007\/3-540-69778-0_32"}],"container-title":["Lecture Notes in Computer Science","KI 2001: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45422-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,24]],"date-time":"2020-04-24T01:17:44Z","timestamp":1587691064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45422-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426127","9783540454229"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45422-5_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"3 September 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}