Equational Axioms of Test Algebra

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 nite 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 nitely axiomatizable ( 25, 6]), so our result does not give us a nite axiomatization of test algebra: in fact, no nite 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.

• Type: Conference
• Year: 1997
• Where: CSL
• Authors: Marco Hollenberg
• Keywords: Automated Reasoning, Axiomatization, CSL 1997, Kleene Algebras, Test Algebra