Kleene 代数 r=0 消除的模块化
计算机科学中的逻辑
2017-01-11 v3
摘要
给定 Kleene 代数中形式为 r = 0 的假设的普遍 Horn 公式，已知我们可以高效地构造一个当且仅当该 Horn 公式有效时才有效的等式。这就是一种假设消除 (elimination of hypotheses)，这在以下方面很有用：因为 Kleene 代数的等式理论是可判定的，而普遍 Horn 理论则不是。我们展示了即使存在其他假设，r = 0 的假设仍然可以被消除。这让我们能够将任何消除假设的技术扩展到包括 r = 0 的假设。
引用
@article{arxiv.cs/0511097,
title = {Modularizing the Elimination of r=0 in Kleene Algebra},
author = {Christopher Hardin},
journal= {arXiv preprint arXiv:cs/0511097},
year = {2017}
}