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

lmcs:2264 - Logical Methods in Computer Science, December 21, 2005, Volume 1, Issue 3
Modularizing the Elimination of r=0 in Kleene Algebra

Authors: Hardin, Christopher

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.


Source : oai:arXiv.org:cs/0511097
DOI : 10.2168/LMCS-1(3:4)2005
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


Share

Consultation statistics

This page has been seen 50 times.
This article's PDF has been downloaded 43 times.