{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:23Z","timestamp":1725533843014},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027154"},{"type":"electronic","value":"9783642027161"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02716-1_11","type":"book-chapter","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T00:22:21Z","timestamp":1246321341000},"page":"138-151","source":"Crossref","is-referenced-by-count":3,"title":["Terminating Tableaux for the Basic Fragment of Simple Type Theory"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning","author":"P.B. Andrews","year":"2001","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 965\u20131007. Elsevier Science, Amsterdam (2001)"},{"issue":"3","key":"11_CR2","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/j.jal.2007.11.001","volume":"6","author":"W.M. Farmer","year":"2008","unstructured":"Farmer, W.M.: The seven virtues of simple type theory. J. Appl. Log.\u00a06(3), 267\u2013286 (2008)","journal-title":"J. Appl. Log."},{"key":"11_CR3","series-title":"Lectures Notes in Mathematics","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/BFb0064870","volume-title":"Proc. Logic Colloquium 1972-73","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Proc. Logic Colloquium 1972-73. Lectures Notes in Mathematics, vol.\u00a0453, pp. 22\u201337. Springer, Heidelberg (1975)"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences\u00a018, 194\u2013211 (1979)","journal-title":"Journal of Computer and System Sciences"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"4","key":"11_CR7","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"P.B. Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.E.: TPS: A hybrid automatic-interactive system for developing proofs. Journal of Applied Logic\u00a04(4), 367\u2013395 (2006)","journal-title":"Journal of Applied Logic"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A cooperative automatic theorem prover for classical higher-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS(LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"11_CR9","unstructured":"Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church\u2019s Type Theory. College Publications (2007)"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"399","DOI":"10.2969\/jmsj\/01940399","volume":"19","author":"M. Takahashi","year":"1967","unstructured":"Takahashi, M.: A proof of cut-elimination theorem in simple type theory. Journal of the Mathematical Society of Japan\u00a019, 399\u2013410 (1967)","journal-title":"Journal of the Mathematical Society of Japan"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"452","DOI":"10.2307\/2270331","volume":"33","author":"D. Prawitz","year":"1968","unstructured":"Prawitz, D.: Hauptsatz for higher order logic. J. Symb. Log.\u00a033, 452\u2013457 (1968)","journal-title":"J. Symb. Log."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-59338-1_43","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"M. Kohlhase","year":"1995","unstructured":"Kohlhase, M.: Higher-order tableaux. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS, vol.\u00a0918, pp. 294\u2013309. Springer, Heidelberg (1995)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/3-540-48660-7_39","volume-title":"Automated Deduction - CADE-16","author":"C. Benzm\u00fcller","year":"1999","unstructured":"Benzm\u00fcller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) CADE 1999. LNCS(LNAI), vol.\u00a01632, pp. 399\u2013413. Springer, Heidelberg (1999)"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02716-1_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:26:26Z","timestamp":1606166786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02716-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027154","9783642027161"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02716-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}