Modularizing the Elimination of r=0 in Kleene Algebra
Logic in Computer Science
2017-01-11 v3
Abstract
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.
Cite
@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}
}