On Action Logic: Equational Theories of Action Algebras

摘要

Pratt (1991, Proceedings of JELIA'90, Volume 478, pp. 97-120) defines action algebras as Kleene algebras with residuals and action logic as the equational theory of action algebras. In contrast to Kleene algebras, action algebras form a (finitely based) variety. Jipsen (2004, Studia Logica, 76, 291-303) proposes a Gentzen-style sequent system for action logic but leaves it as an open question if this system admits cut-elimination and if action logic is decidable. We show that Jipsen's system does not admit cut-elimination. We prove that the equational theory of ~*-continuous action algebras and the simple Horn theory of ~*-continuous Kleene algebras are not recursively enumerable and they possess FMP, but action logic does not possess FMP.