{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:26:20Z","timestamp":1766136380864},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,15]],"date-time":"2013-03-15T00:00:00Z","timestamp":1363305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10817-013-9283-8","type":"journal-article","created":{"date-parts":[[2013,3,14]],"date-time":"2013-03-14T08:55:24Z","timestamp":1363251324000},"page":"57-77","source":"Crossref","is-referenced-by-count":18,"title":["Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems"],"prefix":"10.1007","volume":"51","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,15]]},"reference":[{"key":"9283_CR1","series-title":"Lecture Notes in Artificial Intelligence","first-page":"164","volume-title":"Proceedings of the 17th International Conference on Automated Deduction","author":"PB 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.) Proceedings of the 17th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol.\u00a01831, pp.\u00a0164\u2013169. Springer-Verlag, Pittsburgh, PA (2000)"},{"issue":"4","key":"9283_CR2","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"PB Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. Journal of Applied Logic 4(4), 367\u2013395 (2006)","journal-title":"Journal of Applied Logic"},{"key":"9283_CR3","series-title":"LNCS\/LNAI","first-page":"16","volume-title":"Proceedings of the 5th International Joint Conference Automated Reasoning, IJCAR 2010","author":"J Backes","year":"2010","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: J\u00fcrgen\u00a0Giesl, R.H. (ed.) Proceedings of the 5th International Joint Conference Automated Reasoning, IJCAR 2010, LNCS\/LNAI, vol.\u00a06173, pp.\u00a076\u201390. Springer, Edinburgh, 16\u201319 July 2010"},{"key":"9283_CR4","unstructured":"Benzm\u00fcller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Raedt, L.D., Bessi\u00e8re, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) Frontiers in Artificial Intelligence and Applications, ECAI, vol.\u00a0242, pp.\u00a0163\u2013168. IOS Press (2012)"},{"key":"9283_CR5","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for classical higher-order logic. In: 4th International Joint Conference on Automated Reasoning (IJCAR\u201908), LNCS (LNAI), vol.\u00a05195, pp.\u00a0162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"9283_CR6","unstructured":"Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. thesis, Department of Informatics, T.U. M\u00fcnchen (2012)"},{"key":"9283_CR7","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/BF00881869","volume":"11","author":"WW Bledsoe","year":"1993","unstructured":"Bledsoe, W.W., Feng, G.: Set-Var. J. Autom. Reason. 11, 293\u2013314 (1993)","journal-title":"J. Autom. Reason."},{"key":"9283_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"408","volume-title":"Proceedings of the 18th International Conference on Automated Deduction","author":"CE Brown","year":"2002","unstructured":"Brown, C.E.: Solving for set variables in higher-order theorem proving. In: Voronkov, A. (ed.) Proceedings of the 18th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol.\u00a02392, pp.\u00a0408\u2013422. Springer-Verlag, Copenhagen (2002)"},{"key":"9283_CR9","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT problems. In: Bj\u00f8rner, N., Sofronie-Stockkermans, V. (eds.) CADE\u2014the 23rd International Conference on Automated Deduction, LNCS\/LNAI, vol.\u00a06803, pp.\u00a0147\u2013161. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_13"},{"issue":"2","key":"9283_CR10","first-page":"1","volume":"6","author":"CE Brown","year":"2010","unstructured":"Brown, C.E., Smolka, G.: Analytic tableaux for simple type theory and its first-order fragment. LMCS 6(2), 1-33 (2010)","journal-title":"LMCS"},{"issue":"9","key":"9283_CR11","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011). doi: 10.1145\/1995376.1995394","journal-title":"Commun. ACM"},{"key":"9283_CR12","series-title":"Lecture Notes in Computer Science","first-page":"333","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.) Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol.\u00a02919, pp.\u00a0333\u2013336. Springer, Berlin\/Heidelberg (2004)"},{"key":"9283_CR13","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver\u2014an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, (IJCAR 2008), Lecture Notes in Computer Science, vol.\u00a05195, pp.\u00a0292\u2013298. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"9283_CR14","series-title":"LNCS\/LNAI","first-page":"16","volume-title":"Proceedings of the 5th International Joint Conference Automated Reasoning, IJCAR 2010","author":"K Korovin","year":"2010","unstructured":"Korovin, K., Sticksel, C.: iprover-eq: an instantiation-based theorem prover with equality. In: J\u00fcrgen Giesl, R.H. (ed.) Proceedings of the 5th International Joint Conference Automated Reasoning, IJCAR 2010, LNCS\/LNAI, vol.\u00a06173, pp.\u00a0196\u2013201. Springer, Edinburgh, 16\u201319 July 2010"},{"key":"9283_CR15","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. In: LNCS, vol.\u00a02283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9283_CR16","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) IWIL-2010 (2010)"},{"key":"9283_CR17","doi-asserted-by":"crossref","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, Lecture Notes in Computer Science, vol.\u00a01657, pp.\u00a0179\u2013193. Springer (1999)","DOI":"10.1007\/3-540-48167-2_13"},{"key":"9283_CR18","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1073\/pnas.49.6.828","volume":"49","author":"RM Smullyan","year":"1963","unstructured":"Smullyan, R.M.: A unifying principle in quantification theory. Proc. Natl. Acad. Sci. U.S.A. 49, 828\u2013832 (1963)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"issue":"4","key":"9283_CR19","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF Parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"9283_CR20","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\u2014CASC-J5. AI Commun. 24(1), 75\u201389 (2011)","journal-title":"AI Commun."},{"issue":"1","key":"9283_CR21","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/AIC-2012-0512","volume":"25","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G.: The CADE-23 automated theorem proving system competition\u2014CASC-23. AI Commun. 25(1), 49\u201363 (2012)","journal-title":"AI Commun."},{"issue":"1","key":"9283_CR22","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. J. Form. Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Form. Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9283-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9283-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9283-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,23]],"date-time":"2020-07-23T22:07:29Z","timestamp":1595542049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9283-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,15]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["9283"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9283-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,15]]}}}