{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:04:51Z","timestamp":1725487491482},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665489"},{"type":"electronic","value":"9783540481591"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48159-1_15","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:27:36Z","timestamp":1184603256000},"page":"208-221","source":"Crossref","is-referenced-by-count":4,"title":["Critical Agents Supporting Interactive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"reference":[{"key":"15_CR1","volume-title":"An Introduction To Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"1986","unstructured":"P.B. Andrews. An Introduction To Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, San Diego, CA, USA, 1986."},{"issue":"3","key":"15_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"P.B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. 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":"15_CR3","volume-title":"Proceedings of the 14th Conference on Automated Deduction (CADE-14)","author":"C. Benzm\u00fcller","year":"1997","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. \u03a9Mega: Towards a Mathematical Assistant. In W. McCune, editor, Proceedings of the 14th Conference on Automated Deduction (CADE-14), LNAI, Townsville, Australia, 1997. Springer Verlag, Berlin, Germany."},{"key":"15_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Proceedings of the 15th Conference on Automated Deduction","author":"C. Benzm\u00fcller","year":"1998","unstructured":"C. Benzm\u00fcller and M. Kohlhase. LEO \u2014 a Higher-Order Theorem Prover. In C. Kirchner and H. Kirchner, editors, Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI, pages 139\u2013144, Lindau, Germany, 1998. Springer."},{"key":"15_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0057438","volume-title":"Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the of the 8th International Conference AIMSA\u201998","author":"C. Benzm\u00fcller","year":"1998","unstructured":"C. Benzm\u00fcller and V. Sorge. A Blackboard Architecture for Guiding Interactive Proofs. In F. Giunchiglia, editor, Artificial Intelligence: Methodology, Systems and Applications, Proceedings of the of the 8th International Conference AIMSA\u201998, number 1480 in LNAI, pages 102\u2013114, Sozopol, Bulgaria, October 1998. Springer Verlag, Berlin, Germany."},{"key":"15_CR6","unstructured":"C. Benzm\u00fcller and V. Sorge. Towards Fine-Grained Proof Planning with Critical Agents. In M. Kerber, editor, Informal Proceedings of the Sixth Workshop on Automated Reasoning Bridging the Gap between Theory and Practice in conjunction with AISB\u201999 Convention, pages 20\u201322, Edinburgh, Scotland, 8\u20139 April 1999. extended abstract."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 9th International Conference on Automated Deduction (CADE-9)","author":"A. Bundy","year":"1988","unstructured":"A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction (CADE-9), volume 310 of LNCS, Argonne, IL, USA, 1988. Springer Verlag, Berlin, Germany."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"J. Denzinger and I. Dahn. Cooperating Theorem Provers. In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume 2, pages 483\u2013416. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_14"},{"key":"15_CR9","unstructured":"J. Denzinger D. Fuchs. Knowledge-Based Cooperation between Theorem Provers by TECHS. Seki Report SR-97-11, Fachbereich Informatik, Universit\u00e4t Kaiserslautern, 1997."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"M. Fisher. An Open Approach to Concurrent Theorem Proving. In J. Geller, H. Kitano, and C. Suttner, editors, Parallel Processing for Artificial Intelligence, volume 3. Elsevier\/North Holland, 1997.","DOI":"10.1016\/S0923-0459(97)80011-0"},{"key":"15_CR11","unstructured":"M. Fisher and A. Ireland. Multi-Agent Proof-Planning. In Workshop on Using AI Methods in Deduction at CADE-15, July 6\u20139 1998."},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das Logische Schlie\u00dfen I und II. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"15_CR13","unstructured":"C. Gerber and C.G. Jung. Resource Management for Boundedly Optimal Agent Societies. In Proceedings of the ECAI\u201998 Workshop on Monitoring and Control of Real-Time Intelligent Systems, pages 23\u201328, 1998."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M.J. Gordon","year":"1979","unstructured":"M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of LNCS. Springer Verlag, Berlin, Germany, 1979."},{"key":"15_CR15","volume-title":"Introduction to HOL","author":"M.J.C. Gordon","year":"1993","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, Cambridge, United Kingdom, 1993."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"C.G. Jung. Experimenting with Layered, Resource-Adapting Agents in the Robocup Simulation. In Proceedings of the ROBOCUP\u201998 Workshop, 1998.","DOI":"10.1007\/3-540-48422-1_17"},{"issue":"2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W. McCune","year":"1997","unstructured":"W. McCune and L. Wos. Otter CADE-13 Competition Incarnations. Journal of Automated Reasoning, 18(2):211\u2013220, 1997. Special Issue on the CADE-13 Automated Theorem Proving System Competition.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR18","unstructured":"S.C. Shapiro. Compiling Deduction Rules from a Semantic Network into a Set of Process. In Abstracts of Workshop on Automated Deduction, Cambridge, MA, USA, 1977. MIT. Abstract only."},{"key":"15_CR19","unstructured":"J. Siekmann, S. M. Hess, C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, M. Kohlhase, K. Konrad, E. Melis, A. Meier, and V. Sorge. L\u03a9UI: A Distributed Graphical User Interface for the Interactive Proof System \u03a9MEGA. Submitted to the International Workshop on User Interfaces for Theorem Provers, 1998."},{"key":"15_CR20","volume-title":"Models of Bounded Rationality","author":"H.A. Simon","year":"1982","unstructured":"H.A. Simon. Models of Bounded Rationality. MIT Press, Cambridge, 1982."},{"key":"15_CR21","unstructured":"S. Zilberstein. Models of Bounded Rationality. In AAAI Fall Symposium on Rational Agency, Cambridge, Massachusetts, November 1995."}],"container-title":["Lecture Notes in Computer Science","Progress in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48159-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T01:51:24Z","timestamp":1587779484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48159-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665489","9783540481591"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48159-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}