Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
复制标题
Kleene 代数的左手完备性，通过循环证明
DOI：
10.29007/hzq3
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
D. Pous
中科院分区：
文献类型：
--
作者：
Anupam Das;Amina Doumane;D. Pous
给出了左手Kleene代数公理关于语言包含的完备性的一个新的证明。这个证明比Boffa的证明（它依赖于Krob的完备性结果）和Kozen和Silva最近的证明都要简单得多。我们的证明建立在最近的一个非成立的序列微积分上，它使得显式计算左手Kleene代数所需的不变量成为可能。
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 Boffa (which relies on Krob’s completeness result), and the more recent proof of Kozen and Silva. Our proof builds on a recent non-wellfounded sequent calculus which makes it possible to explicitly compute the invariants required for left-handed Kleene algebra.