TY - GEN
T1 - Designing a Safe Forward Chaining Tactic Using Productive Proofs
AU - Chaudhuri, Kaustuv
AU - Gantait, Arunava
AU - Miller, Dale
N1 - Publisher Copyright:
© The Author(s) 2026.
PY - 2026/1/1
Y1 - 2026/1/1
N2 - We present a proof-theoretic treatment of forward chaining and saturation within a multisorted, first-order intuitionistic logic with equality. The notions of polarity and focused proofs are central to our approach since they provide a characterization of geometric implications as bipolar formulas as well as a natural setting to describe forward chaining and the concept of productive proofs. We identify conditions under which forward chaining with a given set of formulas is guaranteed to saturate in a finite number of steps. The motivation for this research stems, in part, from exploring avenues to 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 and saturation for Abella by presenting examples that compute congruence closure and assist in other equational and relational reasoning tasks.
AB - We present a proof-theoretic treatment of forward chaining and saturation within a multisorted, first-order intuitionistic logic with equality. The notions of polarity and focused proofs are central to our approach since they provide a characterization of geometric implications as bipolar formulas as well as a natural setting to describe forward chaining and the concept of productive proofs. We identify conditions under which forward chaining with a given set of formulas is guaranteed to saturate in a finite number of steps. The motivation for this research stems, in part, from exploring avenues to 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 and saturation for Abella by presenting examples that compute congruence closure and assist in other equational and relational reasoning tasks.
UR - https://www.scopus.com/pages/publications/105019256262
U2 - 10.1007/978-3-032-06085-3_16
DO - 10.1007/978-3-032-06085-3_16
M3 - Conference contribution
AN - SCOPUS:105019256262
SN - 9783032060846
T3 - Lecture Notes in Computer Science
SP - 299
EP - 317
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Proceedings
A2 - Pozzato, Gian Luca
A2 - Uustalu, Tarmo
PB - Springer Science and Business Media Deutschland GmbH
T2 - 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2025
Y2 - 27 September 2025 through 29 September 2025
ER -