{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:29Z","timestamp":1725471149783},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_20","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"220-234","source":"Crossref","is-referenced-by-count":1,"title":["Cut-Simulation in Impredicative Logics"],"prefix":"10.1007","author":[{"given":"Christoph E.","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Chad E.","family":"Brown","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"20_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in type theory. Journal of Symbolic Logic\u00a036(3), 414\u2013432 (1971)","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"20_CR2","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"Andrews, P.B.: General models and extensionality. Journal of Symbolic Logic\u00a037(2), 395\u2013397 (1972)","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)","edition":"2"},{"key":"20_CR4","unstructured":"Benzm\u00fcller, C.E.: Equality and Extensionality in Automated Higher-Order Theorem Proving. PhD thesis, Saarland University (1999)"},{"issue":"4","key":"20_CR5","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C.E. Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C.E., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. Journal of Symbolic Logic\u00a069(4), 1027\u20131088 (2004)","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR6","unstructured":"Benzm\u00fcller, C.E., Brown, C.E., Kohlhase, M.: Semantic techniques for higher-order cut-elimination. Seki Report SR-2004-07, Saarland University (2004)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.E., Brown, C.E., Kohlhase, M.: Cut-simulation in impredicative logics (extended version). Seki Report SR-2006-01, Saarland University (2006)","DOI":"10.1007\/11814771_20"},{"key":"20_CR8","unstructured":"Brown, C.E.: Set Comprehension in Church\u2019s Type Theory. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University (2004)"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR10","first-page":"7","volume":"8","author":"K.J.J. Hintikka","year":"1955","unstructured":"Hintikka, K.J.J.: Form and content in quantification theory. Acta Philosophica Fennica\u00a08, 7\u201355 (1955)","journal-title":"Acta Philosophica Fennica"},{"key":"20_CR11","unstructured":"Huet, G.P.: A mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139\u2013146 (1973)"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"222","DOI":"10.2307\/2369948","volume":"30","author":"B. Russell","year":"1908","unstructured":"Russell, B.: Mathematical logic as based on the theory of types. American Journal of Mathematics\u00a030, 222\u2013262 (1908)","journal-title":"American Journal of Mathematics"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"828","DOI":"10.1073\/pnas.49.6.828","volume":"49","author":"R.M. Smullyan","year":"1963","unstructured":"Smullyan, R.M.: A unifying principle for quantification theory. Proc. Nat. Acad Sciences\u00a049, 828\u2013832 (1963)","journal-title":"Proc. Nat. Acad Sciences"},{"key":"20_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:32Z","timestamp":1605644072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11814771_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}