{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:38:45Z","timestamp":1743061125461,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_13","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T22:21:44Z","timestamp":1311027704000},"page":"147-161","source":"Crossref","is-referenced-by-count":8,"title":["Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","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.: System description: TPS: A theorem proving system for type theory. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 164\u2013169. Springer, Heidelberg (2000)"},{"issue":"4","key":"13_CR2","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":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-14203-1_7","volume-title":"Automated Reasoning","author":"J. Backes","year":"2010","unstructured":"Backes, J., Brown, C.E.: Analytic Tableaux for Higher-Order Logic with Choice. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 76\u201390. Springer, Heidelberg (2010)"},{"key":"13_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C.E. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A cooperative automatic theorem prover for classical higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Brown, C.E., Smolka, G.: Analytic tableaux for simple type theory and its first-order fragment. Logical Methods in Computer Science\u00a06(2) (June 2010)","DOI":"10.2168\/LMCS-6(2:3)2010"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 333\u2013336. Springer, Heidelberg (2004)"},{"key":"13_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-48167-2_13","volume-title":"TYPES","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: Algorithms for equality and unification in the presence of notational definitions. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, pp. 179\u2013193. Springer, Heidelberg (1999)"},{"key":"13_CR9","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 in quantification theory. Proceedings of the National Academy of Sciences, U.S.A\u00a049, 828\u2013832 (1963)","journal-title":"Proceedings of the National Academy of Sciences, U.S.A"},{"issue":"1","key":"13_CR10","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G. Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR Automated Theorem Proving System Competition - CASC-J5. AI Communications\u00a024(1), 75\u201389 (2011)","journal-title":"AI Communications"},{"issue":"1","key":"13_CR11","first-page":"1","volume":"3","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning\u00a03(1), 1\u201327 (2010)","journal-title":"Journal of Formalized Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T11:44:48Z","timestamp":1592739888000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}