{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:26:47Z","timestamp":1725668807152},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,6,16]],"date-time":"2024-06-16T00:00:00Z","timestamp":1718496000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,16]],"date-time":"2024-06-16T00:00:00Z","timestamp":1718496000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,9]]},"DOI":"10.1007\/s10817-024-09703-8","type":"journal-article","created":{"date-parts":[[2024,6,16]],"date-time":"2024-06-16T12:01:33Z","timestamp":1718539293000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic"],"prefix":"10.1007","volume":"68","author":[{"given":"Camillo","family":"Fiorentini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mauro","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,16]]},"reference":[{"key":"9703_CR1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic. Oxford Logic Guides","author":"AV Chagrov","year":"1997","unstructured":"Chagrov, A.V., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides, vol. 35. Oxford University Press, Oxford (1997)"},{"key":"9703_CR2","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/978-3-662-48899-7_43","volume-title":"LPAR-20. LNCS","author":"K Claessen","year":"2015","unstructured":"Claessen, K., Ros\u00e9n, D.: SAT modulo intuitionistic implications. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20. LNCS, vol. 9450, pp. 622\u2013637. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_43"},{"issue":"1","key":"9703_CR3","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44(1), 36\u201350 (1979). https:\/\/doi.org\/10.2307\/2273702","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"9703_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbolic Logic 57(3), 795\u2013807 (1992). https:\/\/doi.org\/10.2307\/2275431","journal-title":"J. Symbolic Logic"},{"key":"9703_CR5","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing, 6th International Conference, SAT. LNCS","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT. LNCS, vol. 2919, pp. 502\u2013518. Springer, Cham (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"9703_CR6","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-16242-8_21","volume-title":"LPAR-17. LNCS","author":"M Ferrari","year":"2010","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: fCube: an efficient prover for intuitionistic propositional logic. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 294\u2013301. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_21"},{"issue":"2","key":"9703_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2159531.2159536","volume":"13","author":"M Ferrari","year":"2012","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: Simplification rules for intuitionistic propositional tableaux. Trans. Comput. Logic 13(2), 14\u201311423 (2012). https:\/\/doi.org\/10.1145\/2159531.2159536","journal-title":"Trans. Comput. Logic"},{"issue":"2","key":"9703_CR8","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-012-9252-7","volume":"51","author":"M Ferrari","year":"2013","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason. 51(2), 129\u2013149 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9252-7","journal-title":"J. Autom. Reason."},{"key":"9703_CR9","doi-asserted-by":"publisher","unstructured":"Fiorentini, C., Ferrari, M.: SAT-based proof search in intermediate propositional logics. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning\u201411th International Joint Conference, IJCAR. LNCS, vol. 13385, pp. 57\u201374. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_5","DOI":"10.1007\/978-3-031-10769-6_5"},{"key":"9703_CR10","doi-asserted-by":"publisher","unstructured":"Fiorentini, C.: An ASP approach to generate minimal countermodels in intuitionistic propositional logic. In: Kraus, S. (eds.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI, pp. 1675\u20131681 (2019). https:\/\/doi.org\/10.24963\/ijcai.2019\/232","DOI":"10.24963\/ijcai.2019\/232"},{"key":"9703_CR11","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-79876-5_13","volume-title":"CADE 28. LNCS","author":"C Fiorentini","year":"2021","unstructured":"Fiorentini, C.: Efficient SAT-based proof search in intuitionistic propositional logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE 28. LNCS, vol. 12699, pp. 217\u2013233. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_13"},{"issue":"3","key":"9703_CR12","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/3372299","volume":"21","author":"C Fiorentini","year":"2020","unstructured":"Fiorentini, C., Ferrari, M.: Duality between unprovability and provability in forward refutation-search for intuitionistic propositional logic. ACM Trans. Comput. Log. 21(3), 22\u201312247 (2020). https:\/\/doi.org\/10.1145\/3372299","journal-title":"ACM Trans. Comput. Log."},{"key":"9703_CR13","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-030-29026-9_7","volume-title":"TABLEAUX 2019. LNCS","author":"C Fiorentini","year":"2019","unstructured":"Fiorentini, C., Gor\u00e9, R., Graham-Lengrand, S.: A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS, vol. 11714, pp. 111\u2013129. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_7"},{"key":"9703_CR14","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:3)2006","author":"JH Gallier","year":"2006","unstructured":"Gallier, J.H.: The completeness of propositional resolution: a simple and constructive proof. Log. Methods Comput. Sci. (2006). https:\/\/doi.org\/10.2168\/LMCS-2(5:3)2006","journal-title":"Log. Methods Comput. Sci."},{"key":"9703_CR15","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-86059-2_5","volume-title":"TABLEAUX 2021. LNCS","author":"R Gor\u00e9","year":"2021","unstructured":"Gor\u00e9, R., Kikkert, C.: CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS, vol. 12842, pp. 74\u201391. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_5"},{"key":"9703_CR16","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-08587-6_19","volume-title":"IJCAR 2014. LNCS","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R., Thomson, J., Wu, J.: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 262\u2013268. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_19"},{"issue":"6","key":"9703_CR17","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL( T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"issue":"1\u20133","key":"9703_CR18","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. J. Autom. Reason. 38(1\u20133), 261\u2013271 (2007). https:\/\/doi.org\/10.1007\/s10817-006-9060-z","journal-title":"J. Autom. Reason."},{"key":"9703_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, vol. 43, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","edition":"2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09703-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09703-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09703-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:08:01Z","timestamp":1725613681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09703-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,16]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9703"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09703-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,6,16]]},"assertion":[{"value":"9 June 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"13"}}