{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:24:08Z","timestamp":1725560648217},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_5","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T15:12:52Z","timestamp":1279638772000},"page":"66-81","source":"Crossref","is-referenced-by-count":6,"title":["A Structured Set of Higher-Order Problems"],"prefix":"10.1007","author":[{"given":"Christoph E.","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Chad E.","family":"Brown","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"5_CR1","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. J. of Symbolic Logic\u00a037(2), 395\u2013397 (1972)","journal-title":"J. of Symbolic Logic"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"P.B. Andrews","year":"1989","unstructured":"Andrews, P.B.: On Connections and Higher Order Logic. J. of Automated Reasoning\u00a05, 257\u2013291 (1989)","journal-title":"J. of Automated Reasoning"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning, ch. 15","author":"P.B. Andrews","year":"2001","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 15, vol.\u00a02, pp. 965\u20131007. Elsevier Science, Amsterdam (2001)"},{"key":"5_CR4","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":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/10721959_11","volume-title":"Automated Deduction - CADE-17","author":"P.B. Andrews","year":"2000","unstructured":"Andrews, P.B., Bishop, M., Brown, C.E.: TPS: A theorem proving system for type theory. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 164\u2013169. Springer, Heidelberg (2000)"},{"issue":"3","key":"5_CR6","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. J. of Symbolic Logic\u00a036(3), 414\u2013432 (1971)","journal-title":"J. of Symbolic Logic"},{"key":"5_CR7","unstructured":"Benzm\u00fcller, C.: Equality and Extensionality in Automated Higher-Order Theorem Proving. PhD thesis, Saarland University (1999)"},{"issue":"4","key":"5_CR8","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C. Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. of Symbolic Logic\u00a069(4), 1027\u20131088 (2004)","journal-title":"J. of Symbolic Logic"},{"key":"5_CR9","unstructured":"Benzm\u00fcller, C., Brown, C.E., Kohlhase, M.: Semantic techniques for higher-order cut-elimination. SEKI Technical Report SR-2004-07, Saarland University, Saarbr\u00fccken, Germany (2004), Available at: \n                    \n                      http:\/\/www.ags.uni-sb.de\/~chris\/papers\/R37.pdf"},{"key":"5_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction - CADE-15","author":"C. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO \u2013 a higher order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 139\u2013144. Springer, Heidelberg (1998)"},{"key":"5_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-540-32275-7_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Benzm\u00fcller","year":"2005","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 415\u2013431. Springer, Heidelberg (2005)"},{"key":"5_CR12","first-page":"9","volume":"20","author":"M.P. Bonacina","year":"1992","unstructured":"Bonacina, M.P., Hsiang, J.: Incompleteness of the RUE\/NRF inference systems. Newsletter of the Association for Automated Reasoning\u00a020, 9\u201312 (1992)","journal-title":"Newsletter of the Association for Automated Reasoning"},{"key":"5_CR13","volume-title":"Logic, Logic, Logic","author":"G. Boolos","year":"1998","unstructured":"Boolos, G.: Logic, Logic, Logic. Harvard University Press, Cambridge (1998)"},{"key":"5_CR14","unstructured":"Brown, C.E.: Set Comprehension in Church\u2019s Type Theory. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University (2004)"},{"key":"5_CR15","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. J. of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"J. of Symbolic Logic"},{"key":"5_CR16","unstructured":"Digricoli, V.J.: Resolution by unification and equality. In: Joyner, W.H. (ed.) Proc. of CADE-4, Austin, Texas, USA (1979)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. of Symbolic Logic\u00a015(2), 81\u201391 (1950)","journal-title":"J. of Symbolic Logic"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G.P. Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science\u00a01, 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"key":"5_CR19","unstructured":"Kohlhase, M.: A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle. PhD thesis, Saarland University (1994)"},{"key":"5_CR20","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)"},{"issue":"8","key":"5_CR21","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J.D. McCharen","year":"1976","unstructured":"McCharen, J.D., Overbeek, R.A., Wos, L.A.: Problems and Experiments for and with Automated Theorem-Proving Programs. IEEE Transactions on Computers\u00a0C-25(8), 773\u2013782 (1976)","journal-title":"IEEE Transactions on Computers"},{"key":"5_CR22","unstructured":"Miller, D.: Proofs in Higher-Order Logic. PhD thesis, Carnegie-Mellon Univ. (1983)"},{"issue":"2","key":"5_CR23","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"Pelletier, F.J.: Seventy-five Problems for Testing Automatic Theorem Provers. J. of Automated Reasoning\u00a02(2), 191\u2013216 (1986)","journal-title":"J. of Automated Reasoning"},{"issue":"2-3","key":"5_CR24","first-page":"79","volume":"15","author":"F.J. Pelletier","year":"2002","unstructured":"Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The Development of CASC. AI Communications\u00a015(2-3), 79\u201390 (2002)","journal-title":"AI Communications"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Prehofer, C.: Solving Higher-Order Equations: From Logic to Programming. Progress in Theoretical Computer Science. Birkh\u00e4user, Basel (1998)","DOI":"10.1007\/978-1-4612-1778-7"},{"key":"5_CR26","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.: Higher-Order Unification Revisited: Complete Sets of Transformations. J. of Symbolic Computation\u00a08, 101\u2013140 (1989)","journal-title":"J. of Symbolic Computation"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R.: The typed \u03bb-calculus is not elementary recursive. Theoretical Computer Science\u00a09, 73\u201381 (1979)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"5_CR28","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library. CNF Release v1.2.1. J. of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"CNF Release v1.2.1. J. of Automated Reasoning"},{"issue":"8","key":"5_CR29","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"C-25","author":"G.A. Wilson","year":"1976","unstructured":"Wilson, G.A., Minker, J.: Resolution, Refinements, and Search Strategies: A Comparative Study. IEEE Transactions on Computers\u00a0C-25(8), 782\u2013801 (1976)","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C.-P. Wirth","year":"2004","unstructured":"Wirth, C.-P.: Descente infinie + Deduction. Logic J. of the IGPL\u00a012(1), 1\u201396 (2004), \n                    \n                      www.ags.uni-sb.de\/~cp\/p\/d\/welcome.html","journal-title":"Logic J. of the IGPL"}],"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\/11541868_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T02:56:33Z","timestamp":1619492193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11541868_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}