Algebraic Proof Theory for Infinitary Action Logic
Logic in Computer Science
2025-01-31 v1 Logic
Abstract
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.
Keywords
Cite
@article{arxiv.2501.18231,
title = {Algebraic Proof Theory for Infinitary Action Logic},
author = {Wesley Fussner and Simon Santschi and Borja Sierra Miranda},
journal= {arXiv preprint arXiv:2501.18231},
year = {2025}
}