{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:08:03Z","timestamp":1725829683968},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_11","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"153-168","source":"Crossref","is-referenced-by-count":1,"title":["Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations"],"prefix":"10.1007","author":[{"given":"Taus","family":"Brock-Nannestad","sequence":"first","affiliation":[]},{"given":"Kaustuv","family":"Chaudhuri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Computation\u00a03(4) (1994)","DOI":"10.1093\/logcom\/4.3.217"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, chapter 2, pp. 19\u201399. Elsevier Science, New York (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"issue":"2","key":"11_CR3","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"M.P. Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. of Automated Reasoning\u00a047(2), 161\u2013189 (2011)","journal-title":"J. of Automated Reasoning"},{"key":"11_CR4","unstructured":"Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University, Technical report CMU-CS-06-162, December 2006"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-16242-8_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K.: Magically constraining the inverse method using dynamic polarity assignment. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 202\u2013216. Springer, Heidelberg (2010)"},{"issue":"2\u20133","key":"11_CR6","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. J. of Automated Reasoning\u00a040(2\u20133), 133\u2013177 (2008)","journal-title":"J. of Automated Reasoning"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38574-2_11","volume-title":"Automated Deduction \u2013 CADE-24","author":"Z. Chihani","year":"2013","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 162\u2013177. Springer, Heidelberg (2013)"},{"key":"11_CR8","unstructured":"Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, Miami, USA (2003)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 179\u2013272. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"issue":"46","key":"11_CR10","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C. Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46), 4747\u20134768 (2009)","journal-title":"Theoretical Computer Science"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-30124-0_36","volume-title":"Computer Science Logic","author":"C. Lynch","year":"2004","unstructured":"Lynch, C.: Unsound theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 473\u2013487. Springer, Heidelberg (2004)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. Technical Report cs.SC\/0310055 (2003)","DOI":"10.2172\/822574"},{"key":"11_CR13","series-title":"Lecture Notes in Artificial Intelligence","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 focused inverse method for intuitionistic propositional logic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 174\u2013181. Springer, Heidelberg (2008)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 230\u2013244. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_19"},{"issue":"1","key":"11_CR15","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), 261\u2013271 (2007)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T23:00:35Z","timestamp":1559257235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}