Hypothesis Elimination in Kleene Semirings
Logic in Computer Science
2014-03-18 v1
Abstract
A Kleene semiring is an algebraic structure satisfying the axioms of Kleene algebra, minus the annihilation axioms (x.0 = 0 = 0.x). We show that Kleene semirings (like Kleene algebras) admit the efficient elimination of various kinds of equational hypotheses, in particular Hoare formulas (t=0, where t is an arbitrary term). Our method is purely proof-theoretic, and can be used to eliminate Horn hypotheses in any suitable Horn-equational theory. Moreover, it gives a simple condition under which hypotheses eliminations can be combined.
Cite
@article{arxiv.1403.4074,
title = {Hypothesis Elimination in Kleene Semirings},
author = {Ernie Cohen},
journal= {arXiv preprint arXiv:1403.4074},
year = {2014}
}