{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:30:13Z","timestamp":1775053813644,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642029585","type":"print"},{"value":"9783642029592","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_19","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T01:02:22Z","timestamp":1248483742000},"page":"230-244","source":"Crossref","is-referenced-by-count":12,"title":["Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method"],"prefix":"10.1007","author":[{"given":"Sean","family":"McLaughlin","sequence":"first","affiliation":[]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"19_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation\u00a02(3), 297\u2013347 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"1-3","key":"19_CR2","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","volume":"107","author":"J.-M. Andreoli","year":"2001","unstructured":"Andreoli, J.-M.: Focussing and proof construction. Annals of Pure and Applied Logic\u00a0107(1-3), 131\u2013163 (2001)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR3","unstructured":"Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University. Technical report CMU-CS-06-162 (December 2006)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11538363_15","volume-title":"Computer Science Logic","author":"K. Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 200\u2013215. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"19_CR5","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10817-007-9091-0","volume":"40","author":"K. Chaudhuri","year":"2008","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning\u00a040(2-3), 133\u2013177 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/B978-044450813-3\/50006-0","volume-title":"Handbook of Automated Reasoning, ch. 4","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 4, vol.\u00a0I, pp. 179\u2013272. Elsevier Science, Amsterdam (2001)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"Graf, P.: Term Indexing. LNCS, vol.\u00a01053. Springer, Heidelberg (1996)"},{"key":"19_CR8","unstructured":"Howe, J.M.: Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St. Andrews, Scotland (1998)"},{"key":"19_CR9","first-page":"464","volume-title":"Logic in Computer Science","author":"F. Lamarche","year":"1995","unstructured":"Lamarche, F.: Games semantics for full propositional linear logic. In: Logic in Computer Science, pp. 464\u2013473. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-540-74915-8_34","volume-title":"Computer Science Logic","author":"C. Liang","year":"2007","unstructured":"Liang, C., Miller, D.: Focusing and polarization in intuitionistic logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 451\u2013465. Springer, Heidelberg (2007)"},{"key":"19_CR11","first-page":"1420","volume":"5","author":"S.Y. Maslov","year":"1964","unstructured":"Maslov, S.Y.: An inverse method for establishing deducibility in classical predicate calculus. Soviet Mathematical Doklady\u00a05, 1420\u20131424 (1964)","journal-title":"Soviet Mathematical Doklady"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-89439-1_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. McLaughlin","year":"2008","unstructured":"McLaughlin, S., Pfenning, F.: Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol.\u00a05330, pp. 174\u2013181. Springer, Heidelberg (2008)"},{"key":"19_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Pientka, B., Li, D.X., Pompigne, F.: Focusing the inverse method for LF: a preliminary report. In: International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (2007)","DOI":"10.1016\/j.entcs.2007.09.020"},{"key":"19_CR15","unstructured":"Raths, T., Otten, J.: The ILTP Library, http:\/\/www.iltp.de"},{"issue":"1-3","key":"19_CR16","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T. Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. Journal of Automated Reasoning\u00a038(1-3), 261\u2013271 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR17","unstructured":"Suttner, C., Sutcliffe, G.: The TPTP problem library: TPTP v2.0.0. Technical Report AR-97-01, Institut f\u00fcr Informatik, TU M\u00fcnchen (1997)"},{"key":"19_CR18","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-61511-3_65","volume-title":"Automated Deduction - Cade-13","author":"T. Tammet","year":"1996","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 2\u201316. Springer, Heidelberg (1996)"},{"key":"19_CR19","first-page":"359","volume-title":"Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"N. Zeilberger","year":"2008","unstructured":"Zeilberger, N.: Focusing and higher-order abstract syntax. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 359\u2013369. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T13:52:02Z","timestamp":1558446722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}