{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:24Z","timestamp":1759017924818,"version":"3.44.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present a proof-theoretic treatment of forward chaining and saturation within a multisorted, first-order intuitionistic logic with equality. The notions of <jats:italic>polarity<\/jats:italic> and <jats:italic>focused proofs<\/jats:italic> are central to\u00a0our approach since they provide a characterization of geometric implications\u00a0as <jats:italic>bipolar formulas<\/jats:italic> as well as a natural setting to describe forward chaining and the concept of <jats:italic>productive proofs<\/jats:italic>. We identify conditions under which forward chaining with a given set\u00a0of formulas is guaranteed to saturate in a finite number of steps. The motivation for this research stems, in part, from exploring avenues\u00a0to automate the Abella theorem prover, which relies on relational specifications, and where theorems in typical proof developments are essentially bipolar formulas. We illustrate the potential benefits of automating forward chaining\u00a0and saturation for Abella by presenting examples that compute congruence closure and assist in other equational and relational reasoning tasks.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_16","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:16Z","timestamp":1758969916000},"page":"299-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Designing a\u00a0Safe Forward Chaining Tactic Using Productive Proofs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2938-547X","authenticated-orcid":false,"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7871-3098","authenticated-orcid":false,"given":"Arunava","family":"Gantait","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0274-4954","authenticated-orcid":false,"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Accattoli, B.: Proof pearl: abella formalization of lambda calculus cube property. In: Hawblitzel, C., Miller, D. (eds.) Second International Conference on Certified Programs and Proofs. LNCS, vol.\u00a07679, pp. 173\u2013187. Springer, Cham (2012)","DOI":"10.1007\/978-3-642-35308-6_15"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Blanc, H., Coen, C.S.: Formalizing functions as processes. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0268, pp. 5:1\u20135:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.5, https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2023\/18380","DOI":"10.4230\/LIPIcs.ITP.2023.5"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992). https:\/\/doi.org\/10.1093\/logcom\/2.3.297","journal-title":"J. Logic Comput."},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., et al.: Abella: a system for reasoning about relational specifications. J. Formalized Reasoning 7(2), 1\u201389 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formalized Reasoning"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.D.: Magic sets and other strange ways to implement logic programs. In: Silberschatz, A. (ed.) Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, pp. 1\u201315. ACM (1986). https:\/\/doi.org\/10.1145\/6012.15399","DOI":"10.1145\/6012.15399"},{"key":"16_CR6","unstructured":"Chaudhuri, K., Gantait, A., Miller, D.: Designing a safe forward chaining tactic using productive proofs. Tech. rep., Inria (2025). https:\/\/hal.archives-ouvertes.fr\/hal-05157939"},{"issue":"2","key":"16_CR7","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1093\/logcom\/exu030","volume":"26","author":"K Chaudhuri","year":"2016","unstructured":"Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Logic Comput. 26(2), 577\u2013603 (2016). https:\/\/doi.org\/10.1093\/logcom\/exu030","journal-title":"J. Logic Comput."},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Lima, L., Reis, G.: Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci. 781, 24\u201338 (2019). https:\/\/doi.org\/10.1016\/j.tcs.2019.02.023. logical and Semantic Frameworks with Applications","DOI":"10.1016\/j.tcs.2019.02.023"},{"key":"16_CR9","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-0-387-09680-3_26","volume-title":"Fifth Ifip International Conference On Theoretical Computer Science \u2013 Tcs 2008","author":"K Chaudhuri","year":"2008","unstructured":"Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multi-focusing. In: Ausiello, G., Karhum\u00e4ki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 383\u2013396. Springer, Boston, MA (2008). https:\/\/doi.org\/10.1007\/978-0-387-09680-3_26"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reasoning 40(2-3), 133\u2013177 (2008). https:\/\/doi.org\/10.1007\/s10817-007-9091-0","DOI":"10.1007\/s10817-007-9091-0"},{"issue":"02","key":"16_CR11","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Log. 21(02), 123\u2013163 (2015)","journal-title":"Bull. Symb. Log."},{"issue":"6","key":"16_CR12","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/155090.155113","volume":"28","author":"C Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. ACM SIGPLAN Notices 28(6), 237\u2013247 (1993). https:\/\/doi.org\/10.1145\/155090.155113","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.ic.2010.09.004","volume":"209","author":"A Gacek","year":"2011","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48\u201373 (2011). https:\/\/doi.org\/10.1016\/j.ic.2010.09.004","journal-title":"Inf. Comput."},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1935). https:\/\/doi.org\/10.1007\/BF01201353. translation of articles that appeared in 1934-35. Collected papers appeared in 1969","DOI":"10.1007\/BF01201353"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoret. Comput. Sci. 410(46), 4747\u20134768 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.07.041. Abstract Interpretation and Logic Programming: A Special Issue in Honor of Professor Giorgio Levi","DOI":"10.1016\/j.tcs.2009.07.041"},{"issue":"1","key":"16_CR16","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0743-1066(86)90004-X","volume":"3","author":"J Lloyd","year":"1986","unstructured":"Lloyd, J., Topor, R.: A basis for deductive database systems II. J. Log. Program. 3(1), 55\u201367 (1986). https:\/\/doi.org\/10.1016\/0743-1066(86)90004-X","journal-title":"J. Log. Program."},{"issue":"5","key":"16_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2022.103091","volume":"173","author":"S Marin","year":"2022","unstructured":"Marin, S., Miller, D., Pimentel, E., Volpe, M.: From axioms to synthetic inference rules via focusing. Ann. Pure Appl. Logic 173(5), 1\u201332 (2022). https:\/\/doi.org\/10.1016\/j.apal.2022.103091","journal-title":"Ann. Pure Appl. Logic"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 91\u2013119 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00171-1","journal-title":"Theoret. Comput. Sci."},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Miller, D.: A survey of the proof-theoretic foundations of logic programming. Theory Pract. Logic Program. 22(6), 859\u2013904 (2022). https:\/\/doi.org\/10.1017\/S1471068421000533. published online November 2021","DOI":"10.1017\/S1471068421000533"},{"issue":"4","key":"16_CR20","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Logic 6(4), 749\u2013783 (2005). https:\/\/doi.org\/10.1145\/1094622.1094628","journal-title":"ACM Trans. Comput. Logic"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Miller, D., Wu, J.H.: A positive perspective on term representations. In: Klin, B., Pimentel, E. (eds.) 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0252, pp. 3:1\u20133:21. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2023.3","DOI":"10.4230\/LIPIcs.CSL.2023.3"},{"key":"16_CR22","unstructured":"Naughton, J.F., Ramakrishnan, R.: Bottom-up evaluation of logic programs. In: Lassez, J., Plotkin, G.D. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 640\u2013700. The MIT Press (1991)"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Negri, S.: Contraction-free sequent calculi for geometric theories with an application to Barr\u2019s theorem. Arch. Math. Logic 42, 389\u2013401 (2003). https:\/\/doi.org\/10.1007\/s001530100124","DOI":"10.1007\/s001530100124"},{"issue":"4","key":"16_CR24","doi-asserted-by":"publisher","first-page":"418","DOI":"10.2307\/420956","volume":"4","author":"S Negri","year":"1998","unstructured":"Negri, S., Plato, J.: Cut elimination in the presence of axioms. Bull. Symbolic Logic 4(4), 418\u2013435 (1998). https:\/\/doi.org\/10.2307\/420956","journal-title":"Bull. Symbolic Logic"},{"key":"16_CR25","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, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"16_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logics","author":"L Vigan\u00f2","year":"2000","unstructured":"Vigan\u00f2, L.: Labelled Non-Classical Logics. Kluwer Academic Publishers, Dordrecht (2000)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:17Z","timestamp":1758969917000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}