{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:28Z","timestamp":1761611188076},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649939"},{"type":"electronic","value":"9783540497936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0057438","type":"book-chapter","created":{"date-parts":[[2006,7,31]],"date-time":"2006-07-31T00:47:47Z","timestamp":1154306867000},"page":"102-114","source":"Crossref","is-referenced-by-count":7,"title":["A blackboard architecture for guiding interactive proofs"],"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":[[2006,6,27]]},"reference":[{"key":"9_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":"9_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":"9_CR3","volume-title":"\u03a9Mega: Towards a Mathematical Assistant","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":"9_CR4","unstructured":"R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"L. D. Erman, F. Hayes-Roth, and R. D. Reddy. The HERSAY-II speech understanding system: Integrating knowledge to resolve uncertainty. ACM Computing Surveys, 12(2), 1980.","DOI":"10.1145\/356810.356816"},{"key":"9_CR6","unstructured":"L. Erman, P. London, and S. Fickas. The Design and an Example Use of HEARSAY-III. In P. J. Hayes, editor, Proceedings of the 7th International Joint Conference on Artificial Intelligence (IJCAI '81), pages 409\u2013415. William Kaufmann, 1981."},{"key":"9_CR7","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\\en I und II. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"9_CR8","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":"9_CR9","doi-asserted-by":"crossref","unstructured":"M. A. P\u00e9rez and J. L. Sibert. Focus in graphical user interfaces. In W. D. Gray, William E. Hefley, and Dianne Murray, editors, Proceedings of the International Workshop on Intelligent User Interfaces, pages 255\u2013258. ACM Press, 1993.","DOI":"10.1145\/169891.170022"},{"key":"9_CR10","unstructured":"The Oz Programming System Programming Systems Lab, DFKI, Germany, 1998. URL: http:\/\/www.ps.uni-sb.de\/oz\/."},{"key":"9_CR11","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 \u03a9\n                mega. Submitted to the International Workshop on User Interfaces for Theorem Provers, 1998."},{"key":"9_CR12","series-title":"ACM Press Frontier Series","volume-title":"Intelligent User Interfaces","year":"1991","unstructured":"J. W. Sullivan and S. W. Tyler, editors. Intelligent User Interfaces. ACM Press Frontier Series. ACM Press, New York, NY, USA, 1991."},{"key":"9_CR13","volume-title":"Real Theorem Provers Deserve Real User-Interfaces","author":"L. Th\u00e9ry","year":"1992","unstructured":"L. Th\u00e9ry, Y. Bertot, and G. Kahn. Real Theorem Provers Deserve Real User-Interfaces. In Proceedings of The Fifth ACM Symposium on Software Development Environments (SDE5), Washington D.C., USA, December 1992. ACM Press."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence: Methodology, Systems, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0057438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T15:23:05Z","timestamp":1549898585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0057438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649939","9783540497936"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0057438","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}