Christopher Hardin - Modularizing the Elimination of r=0 in Kleene Algebra

lmcs:2264 - Logical Methods in Computer Science, December 21, 2005, Volume 1, Issue 3 - https://doi.org/10.2168/LMCS-1(3:4)2005
Modularizing the Elimination of r=0 in Kleene AlgebraArticle

Authors: Christopher Hardin

    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.


    Volume: Volume 1, Issue 3
    Published on: December 21, 2005
    Submitted on: April 20, 2005
    Keywords: Computer Science - Logic in Computer Science,F.3.1
    Funding:
      Source : OpenAIRE Graph
    • Kleene Algebra; Funder: National Science Foundation; Code: 0105586

    2 Documents citing this article

    Consultation statistics

    This page has been seen 877 times.
    This article's PDF has been downloaded 334 times.