Rewriting Extended Regular Expressions

We consider an extended algebra of regular events (languages) with intersection besides the usual operations. This algebra has the structure of a distributive lattice with monotonic operations; the latter property is crucial for some applications. We give a new complete Horn equational axiomatization of the algebra and develop some term-rewriting techniques for constructing logical inferences of valid equations