Modularizing the Elimination of r=0 in Kleene Algebra

TL;DR

This paper presents a modular approach to eliminate hypotheses of the form r=0 in Kleene algebra, extending existing techniques to handle these specific hypotheses while preserving decidability.

Contribution

It introduces a method to modularly eliminate r=0 hypotheses in Kleene algebra even when other hypotheses are present, broadening the applicability of hypothesis elimination techniques.

Findings

Hypotheses of the form r=0 can be eliminated alongside other hypotheses.

The approach preserves the decidability of the equational theory.

Extends existing hypothesis elimination methods to include r=0 hypotheses.

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.