.png){kind=icon}
.png){kind=icon}
Return
Designing a Safe Forward Chaining Tactic Using Productive Proofs
.png){kind=icon}
OA
AI
DOI：10.1007/978-3-032-06085-3_16.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
SEQUENT CALCULI
CUT-ELIMINATION
SYSTEM
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
A
IF:
0
Papers:
25
Citations:
0