{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:17:34Z","timestamp":1750306654245,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,1]],"date-time":"2015-03-01T00:00:00Z","timestamp":1425168000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:p>It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the na\u00efve goal-oriented proof-search strategy, consisting in applying the rules of the calculus bottom up until possible, can generate branches of infinite length. The usual solution to this problem is to support the proof-search procedure with a loop checking mechanism that prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development.<\/jats:p><jats:p>In this article, we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism that, analyzing only the current goal of the proof search, allows one to drive the application of rules to guarantee termination and to avoid useless backtracking. We describe an evaluation-driven proof-search procedure that given a sequent \u03c3 returns either a G3i-derivation of \u03c3 or a countermodel for \u03c3. We prove that such a procedure is terminating and correct, and that the depth of the G3i-trees generated during proof search is quadratic in the size of \u03c3. Finally, we discuss the overhead time introduced by evaluation functions in the proof-search procedure.<\/jats:p>","DOI":"10.1145\/2660770","type":"journal-article","created":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T16:03:43Z","timestamp":1427299423000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["An Evaluation-Driven Decision Procedure for G3i"],"prefix":"10.1145","volume":"16","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi dell'Insubria"}]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano"}]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano-Bicocca"}]}],"member":"320","published-online":{"date-parts":[[2015,3,24]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"S. Buss and R. Iemhoff. 2003. The depth of intuitionistic cut free proofs. Manuscript. S. Buss and R. Iemhoff. 2003. The depth of intuitionistic cut free proofs. Manuscript."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"A. Chagrov and M. Zakharyaschev. 1997. Modal Logic. Oxford University Press. A. Chagrov and M. Zakharyaschev. 1997. Modal Logic. Oxford University Press.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_11"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1203350782"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275431"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780342_19"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.19.149-166"},{"key":"e_1_2_1_8_1","volume-title":"Lecture Notes in Computer Science","volume":"6397","author":"Ferrari M.","unstructured":"M. Ferrari , C. Fiorentini , and G. Fiorino . 2010. FCube: An efficient prover for intuitionistic propositional logic. In Logic for Programming, Artificial Intelligence, and Reasoning . Lecture Notes in Computer Science , Vol. 6397 . Springer, 294--301. M. Ferrari, C. Fiorentini, and G. Fiorino. 2010. FCube: An efficient prover for intuitionistic propositional logic. In Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science, Vol. 6397. Springer, 294--301."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2159531.2159536"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9252-7"},{"key":"e_1_2_1_11_1","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science","volume":"8123","author":"Ferrari M.","unstructured":"M. Ferrari , C. Fiorentini , and G. Fiorino . 2013b. A terminating evaluation-driven variant of G3i . In Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science , Vol. 8123 . Springer, 104--118. M. Ferrari, C. Fiorentini, and G. Fiorino. 2013b. A terminating evaluation-driven variant of G3i. In Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, Vol. 8123. Springer, 104--118."},{"volume-title":"Algorithmic Aspects of Intuitionistic Propositional Logic. SICS Report R87010B","author":"Franz\u00e9n T.","key":"e_1_2_1_12_1","unstructured":"T. Franz\u00e9n . 1988. Algorithmic Aspects of Intuitionistic Propositional Logic. SICS Report R87010B . Swedish Institute of Computer Science . T. Franz\u00e9n. 1988. Algorithmic Aspects of Intuitionistic Propositional Logic. SICS Report R87010B. Swedish Institute of Computer Science."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"D. Gabbay and N. Olivetti. 2000. Goal-Directed Proof Theory. Springer. D. Gabbay and N. Olivetti. 2000. Goal-Directed Proof Theory. Springer.","DOI":"10.1007\/978-94-017-1713-7"},{"volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen G.","key":"e_1_2_1_14_1","unstructured":"G. Gentzen . 1969. Investigations into logical deduction . In The Collected Papers of Gerhard Gentzen , M. E. Szabo (Ed.). North Holland , Amsterdam . G. Gentzen. 1969. Investigations into logical deduction. In The Collected Papers of Gerhard Gentzen, M. E. Szabo (Ed.). North Holland, Amsterdam."},{"key":"e_1_2_1_15_1","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science","volume":"1071","author":"Heuerding A.","unstructured":"A. Heuerding , M. Seyfried , and H. Zimmermann . 1996. Efficient loop-check for backward proof search in some non-classical propositional logics . In Theorem Proving with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science , Vol. 1071 . Springer, 210--225. A. Heuerding, M. Seyfried, and H. Zimmermann. 1996. Efficient loop-check for backward proof search in some non-classical propositional logics. In Theorem Proving with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, Vol. 1071. Springer, 210--225."},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Howe J.","unstructured":"J. Howe . 1997. Two loop detection mechanisms: A comparision . In Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Computer Science , Vol. 1227 . Springer , 188--200. J. Howe. 1997. Two loop detection mechanisms: A comparision. In Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, Vol. 1227. Springer, 188--200."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.1.63"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Simplification: A general constraint propagation technique for propositional and modal tableaux. In Automated Reasoning with Analytic Tableaux and Related Methods","author":"Massacci F.","year":"1998","unstructured":"F. Massacci . 1998 . Simplification: A general constraint propagation technique for propositional and modal tableaux. In Automated Reasoning with Analytic Tableaux and Related Methods . Lecture Notes in Computer Science , Vol. 1397 . Springer , 217--231. F. Massacci. 1998. Simplification: A general constraint propagation technique for propositional and modal tableaux. In Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, Vol. 1397. Springer, 217--231."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/5.1.145"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.12.008"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"L. Pinto and R. Dyckhoff. 1995. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana M. Behara R. Fritsch and R. Lintz (Eds.). Walter de Gruyter Berlin 225--232. L. Pinto and R. Dyckhoff. 1995. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana M. Behara R. Fritsch and R. Lintz (Eds.). Walter de Gruyter Berlin 225--232.","DOI":"10.1515\/9783110886726.225"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.5.619"},{"key":"e_1_2_1_24_1","volume-title":"Cambridge Tracts in Theoretical Computer Science","volume":"43","author":"Troelstra A.","unstructured":"A. Troelstra and H. Schwichtenberg . 2000. Basic Proof Theory (2nd ed.) . Cambridge Tracts in Theoretical Computer Science , Vol. 43 . Cambridge University Press. A. Troelstra and H. Schwichtenberg. 2000. Basic Proof Theory (2nd ed.). Cambridge Tracts in Theoretical Computer Science, Vol. 43. Cambridge University Press."},{"volume-title":"Sixteen Papers on Logic and Algebra","author":"Vorob\u2019ev N. N.","key":"e_1_2_1_25_1","unstructured":"N. N. Vorob\u2019ev . 1970. A new algorithm of derivability in a constructive calculus of statements . In Sixteen Papers on Logic and Algebra . American Mathematical Society Translations: Series 2, Vol. 94 . American Mathematical Society , Providence, RI, 37--71. N. N. Vorob\u2019ev. 1970. A new algorithm of derivability in a constructive calculus of statements. In Sixteen Papers on Logic and Algebra. American Mathematical Society Translations: Series 2, Vol. 94. American Mathematical Society, Providence, RI, 37--71."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660770","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2660770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:56:13Z","timestamp":1750229773000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2660770"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1145\/2660770"],"URL":"https:\/\/doi.org\/10.1145\/2660770","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2015,3]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}