On Action Logic: Equational Theories of Action Algebras
- 23 August 2006
- journal article
- research article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 17 (1) , 199-217
- https://doi.org/10.1093/logcom/exl036
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: