Kleene代数中r=0消去的模化
Modularizing the Elimination of r=0 in Kleene Algebra
摘要：
已知Kleene代数的一个通用Horn公式，在r = 0的假设下，我们可以有效地构造一个方程，该方程成立当且仅当Horn公式成立.这是一<i>个消除假设</i>的例子，这是有用的，因为Kleene代数的方程理论是可判定的，而通用Horn理论不是。我们表明，假设的形式r = 0仍然可以消除在其他假设的存在。这使我们可以扩展任何用于消除假设的技术，以包括r = 0形式的假设。
英文摘要：
Given a universal Horn formula of Kleene algebra with hypotheses of the form r = 0, it is already known that we can efficiently construct an equation which is valid if and only if the Horn formula is valid. This is an example of <i>elimination of hypotheses</i>, which is useful because the equational theory of Kleene algebra is decidable while the universal Horn theory is not. We show that hypotheses of the form r = 0 can still be eliminated in the presence of other hypotheses. This lets us extend any technique for eliminating hypotheses to include hypotheses of the form r = 0.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
