Algebraic Proof Theory for Infinitary Action Logic
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917906781044736 |
|---|---|
| author | Fussner, Wesley Santschi, Simon Miranda, Borja Sierra |
| author_facet | Fussner, Wesley Santschi, Simon Miranda, Borja Sierra |
| contents | We exhibit a uniform method for obtaining (wellfounded and non-wellfounded) cut-free sequent-style proof systems that are sound and complete for various classes of action algebras, i.e., Kleene algebras enriched with meets and residuals. Our method applies to any class of *-continuous action algebras that is defined, relative to the class of all *-continuous action algebras, by analytic quasiequations. The latter make up an expansive class of conditions encompassing the algebraic analogues of most well-known structural rules. These results are achieved by wedding existing work on non-wellfounded proof theory for action algebras with tools from algebraic proof theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_18231 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Algebraic Proof Theory for Infinitary Action Logic Fussner, Wesley Santschi, Simon Miranda, Borja Sierra Logic in Computer Science Logic 03F05 (Primary) 03F52, 68Q70 (Secondary) F.3.0 We exhibit a uniform method for obtaining (wellfounded and non-wellfounded) cut-free sequent-style proof systems that are sound and complete for various classes of action algebras, i.e., Kleene algebras enriched with meets and residuals. Our method applies to any class of *-continuous action algebras that is defined, relative to the class of all *-continuous action algebras, by analytic quasiequations. The latter make up an expansive class of conditions encompassing the algebraic analogues of most well-known structural rules. These results are achieved by wedding existing work on non-wellfounded proof theory for action algebras with tools from algebraic proof theory. |
| title | Algebraic Proof Theory for Infinitary Action Logic |
| topic | Logic in Computer Science Logic 03F05 (Primary) 03F52, 68Q70 (Secondary) F.3.0 |
| url | https://arxiv.org/abs/2501.18231 |