{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:40Z","timestamp":1725494320257},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_40","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"414-428","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Generation of Proof Search Strategies for Second-Order Logic"],"prefix":"10.1007","author":[{"given":"Raul H. C.","family":"Lopes","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"40_CR1","doi-asserted-by":"crossref","unstructured":"Peter B. Andrews, Dale A. Miller, Eve L. Cohen, and Frank Pfenning, Automating higher-order logic, In Bledsoe and Loveland [4], pp. 169\u2013192.","DOI":"10.1090\/conm\/029\/09"},{"key":"40_CR2","first-page":"255","volume":"66","author":"D. Angluin","year":"1989","unstructured":"Dana Angluin, William Gasarch, and Carl H. Smith, Training sequences, Theoretical Computer Science 66 (1989), 255\u2013272.","journal-title":"Training sequences"},{"key":"40_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BF00881869","volume":"11","author":"W.W. Bledsoe","year":"1993","unstructured":"W.W. Bledsoe and Guohui Feng, Set-var, Journal of Automated Reasoning 11 (1993), 293\u2013314.","journal-title":"Journal of Automated Reasoning"},{"key":"40_CR4","doi-asserted-by":"crossref","unstructured":"W.W. Bledsoe and D.W. Loveland (eds.), Automated theorem proving: After 25 years, American Mathematical Society, Providence-Rhode Island, 1984.","DOI":"10.1090\/conm\/029"},{"key":"40_CR5","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 (1940), 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"40_CR6","doi-asserted-by":"publisher","first-page":"303","DOI":"10.2307\/421033","volume":"4","author":"J. Hintikka","year":"1998","unstructured":"Jaakko Hintikka, Truth definition, Skolem functions, and axiomatic set theory, The Bulletin of Symbolic Logic 4 (1998), no. 3, 303\u2013337.","journal-title":"The Bulletin of Symbolic Logic"},{"key":"40_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G\u00e9rard P. Huet, A unification algorithm for typed \u03bb-calculus,Theoretical Computer Science 1 (1975), 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"40_CR8","unstructured":"Stephen Cole Kleene, Permutability of inferences in Gentzen\u2019s calculi LK and LJ, Memoirs of the AMS, vol. 10, American Mathematical Society, 1952."},{"key":"40_CR9","unstructured":"Raul H.C. Lopes, Inducing search methods from proofs, Tech. report, School of Computer Studies, University of Leeds, 1997."},{"key":"40_CR10","unstructured":"Raul Henriques Cardoso Lopes, Inductive generalization of proof search strategies from examples, Ph.D. thesis, University of Leeds, 1998."},{"key":"40_CR11","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"4","author":"D. A. Miller","year":"1987","unstructured":"Dale A. Miller, iCompact representation of proofs, Studia Logica 4 (1987), 347\u2013370.","journal-title":"Studia Logica"},{"key":"40_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. A. Miller","year":"1992","unstructured":"\u2014, Unification under a mixed prefix, Journal of Symbolic Computation 14 (1992), 321\u2013358.","journal-title":"Journal of Symbolic Computation"},{"key":"40_CR13","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0004-3702(82)90040-6","volume":"18","author":"T. M. Mitchell","year":"1982","unstructured":"Tom M. Mitchell, Generalization as search, Artificial Intelligence 18 (1982), 203\u2013226.","journal-title":"Artificial Intelligence"},{"key":"40_CR14","doi-asserted-by":"crossref","unstructured":"N. Shankar, Proof search in the intuitionistic sequent calculus, In Stickel [15], LNAI, 449, pp. 522\u2013536.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"M.E. Stickel (ed.), Proceedings of the 10th International Conference on Automated Deduction, Springer-Verlag, 1990, LNAI, 449.","DOI":"10.1007\/3-540-52885-7"},{"key":"40_CR16","unstructured":"Mark Tarver, An algorithm for inducing tactics from sequentzen proofs, Workshop on practical applications of automated reasoning, 1995, AISB."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:40Z","timestamp":1556945800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}