Equational Axioms of Test Algebra
Marco Hollenberg · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1996
We present a complete axiomatization of test algebra ([24,18,29]), the two-sorted algebraic variant of Propositional Dynamic Logic (PDL,[21,7]). The axiomatization consists of adding a finite number of equations to any axiomatization of Kleene algebra ([15,26,17,4]) and algebraic translations of the Segerberg ([27]) axioms for PDL. Kleene algebras are not finitely axiomatizable ([25,6]), so our result does not give us a finite axiomatization of test algebra: in fact, no finite equational axiomatization exists. We also present a single-sorted version of test algebra, using the notion of dynamic negation ([9,2,11]), to which the previous results carry over.