zbMATH — the first resource for mathematics

Left-handed completeness for Kleene algebra, via cyclic proofs. (English) Zbl 1415.68124
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 271-289 (2018).
Summary: We give a new proof that the axioms of left-handed Kleene algebra are complete with respect to language containments. This proof is significantly simpler than both the proof of M. Boffa (which relies on Krob’s completeness result) [RAIRO, Inform. Théor. Appl. 29, No. 6, 515–518 (1995; Zbl 0881.68071)], and the more recent proof of D. Kozen and A. Silva [Lect. Notes Comput. Sci. 7560, 162–178 (2012; Zbl 1364.68268)]. Our proof builds on a recent non-well-founded sequent calculus which makes it possible to explicitly compute the invariants required for left-handed Kleene algebra.
For the entire collection see [Zbl 1407.68021].

68Q45 Formal languages and automata
03B70 Logic in computer science
Full Text: DOI