Kleene algebras, adjunction and structural control
Giuseppe Greco, Fei Liang, Alessandra Palmigiano
TL;DR
This paper introduces a multi-type calculus for measurable Kleene algebras, establishing key logical properties and leveraging ideas from formal linguistics related to structural control.
Contribution
It develops a novel multi-type calculus for measurable Kleene algebras, integrating concepts from formal linguistics to enhance logical analysis.
Findings
Proves soundness and completeness of the calculus
Establishes cut elimination and subformula property
Demonstrates conservativity of the calculus
Abstract
In the present paper, we introduce a multi-type calculus for the logic of measurable Kleene algebras, for which we prove soundness, completeness, conservativity, cut elimination and subformula property. Our proposal imports ideas and techniques developed in formal linguistics around the notion of structural control.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems