{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:47Z","timestamp":1749124067354},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055140","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"245-261","source":"Crossref","is-referenced-by-count":4,"title":["Hot: A concurrent automated theorem prover based on higher-order tableaux"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Konrad","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"3","key":"15_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"},{"doi-asserted-by":"crossref","unstructured":"Peter B. Andrews, 1973. letter to Roger Hindley dated January 22, 1973.","key":"15_CR2","DOI":"10.2307\/2346933"},{"unstructured":"H. P. Barendregt. The Lambda Calculus. North Holland, 1984.","key":"15_CR3"},{"key":"15_CR4","first-page":"252","volume-title":"number 1249 in LNAI","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. \u03a9 Mega: Towards a mathematical assistant. In William McCune, editor, Proceedings of the 14th Conference on Automated Deduction, number 1249 in LNAI, pages 252\u2013255, Townsville, Australia, 1997. Springer Verlag."},{"unstructured":"Christoph Benzm\u00fcller, 1997. LEO benchmarks http:\/\/www.ags.uni-sb.de\/projects\/deduktion\/projects\/hot\/mizar\/.","key":"15_CR5"},{"key":"15_CR6","volume-title":"Research Report 97-198","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Christoph Benzm\u00fcller. A Calculus and a System Architecture for Extensional Higher-Order Resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh,USA, June 1997."},{"unstructured":"Maria Paola Bonacina and Jieh Hsiang. Parallelization of Deduction Strategies: An Analytical Study. Journal of Automated Reasoning, (13):1\u201333, 1994.","key":"15_CR7"},{"unstructured":"Christoph Benzm\u00fcller and Michael Kohlhase. Resolution for henkin models. SEKI-Report SR-97-10, Universit\u00c4t des Saarlandes, 1997.","key":"15_CR8"},{"issue":"3","key":"15_CR9","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"Bernhard Beckert and Joachim Posegga. Lean, Tableau-based Deduction. Journal of Automated Reasoning, 15(3):339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"unstructured":"Ingo Dahn, 1997. Statistics for Problems from the Mizar Library. http:\/\/www-irm.mathematik.hu-berlin.de\/~ilf\/miz2atp\/mizstat.html.","key":"15_CR11"},{"unstructured":"R. Engelmore and T. Morgan, editors. Blackboard Systems. Addison-Wesley, 1988.","key":"15_CR12"},{"doi-asserted-by":"crossref","unstructured":"Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer Verlag, 1990.","key":"15_CR13","DOI":"10.1007\/978-1-4684-0357-2"},{"unstructured":"Claire Gardent, Michael Kohlhase, and Karsten Konrad. Higher-order coloured unification: a linguistic application. Submitted for publication, 1997.","key":"15_CR14"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"Kurt G\u00f6del. \u00fcber formal unentscheidbare S\u00c4tze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik, 38:173\u2013198, 1931. English Version in [27].","journal-title":"Monatshefte der Mathematischen Physik"},{"issue":"67","key":"15_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"1","author":"J. H. Gallier","year":"1989","unstructured":"Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 1(67):203\u2013260, 1989.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81\u201391, 1950.","journal-title":"Journal of Symbolic Logic"},{"unstructured":"Dieter Hutter and Michael Kohlhase. A coloured version of the \u03bb-calculus. SEKI-Report SR-95-05, Universit\u00c4t des Saarlandes, 1995.","key":"15_CR18"},{"unstructured":"Michael Kohlhase and Karsten Konrad. Higher-order automated theorem proving for natural language semantics. Seki Report SR-98-04, Fachbereich Informatik, Universit\u00c4t Saarbr\u00fccken, 1998.","key":"15_CR19"},{"doi-asserted-by":"crossref","unstructured":"Michael Kohlhase. Higher-order tableaux. In Proceedings of the Tableau Workshop, pages 294\u2013309, Koblenz, Germany, 1995.","key":"15_CR20","DOI":"10.1007\/3-540-59338-1_43"},{"unstructured":"Michael Kohlhase. Higher-order automated theorem proving. In Wolfgang Bibel and Peter Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume 2. Kluwer, 1998. forthcoming.","key":"15_CR21"},{"doi-asserted-by":"crossref","unstructured":"Luiz V. Leao and Sarosh N. Talukdar. COPS: A System for Constructing Multiple Blackboards. In Alan H. Bond and Les Gasser, editors, Readings in Distributed Artificial Intelligence, page 547ff. Morgan Kaufmann, 1988.","key":"15_CR22","DOI":"10.1016\/B978-0-934613-63-7.50054-1"},{"unstructured":"Dale Miller. Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon University, 1983.","key":"15_CR23"},{"unstructured":"Programming Systems Lab Saarbr\u00fccken, 1998. The Oz Webpage: http:\/\/www.ps.uni-sb.de\/oz\/.","key":"15_CR24"},{"doi-asserted-by":"crossref","unstructured":"Gert Smolka. The oz programming model. In Jan van Leeuwen, editor, Computer Science Today, volume 1000 of LNCS, pages 324\u2013343. Springer Verlag, 1995.","key":"15_CR25","DOI":"10.1007\/BFb0015252"},{"unstructured":"Z. Trybulec and H. Swieczkowska. Boolean properties of sets. Journal of Formalized Mathematics, 1, 1989.","key":"15_CR26"},{"unstructured":"Jean van Heijenoort, editor. From Frege to G\u00f6del A Source Book in Mathematical Logic, 1879\u20131931. Source Books in the History of the Sciences. Harvard University Press, 1967.","key":"15_CR27"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055140","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,5]],"date-time":"2024-02-05T15:54:56Z","timestamp":1707148496000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055140"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0055140","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}