An Infinitary Sequent System for the Equational Theory of *-continuous Action Lattices

Article type: Research Article

Authors: Palka, Ewa

Affiliations: Faculty of Mathematics and Computer Science, Adam Mickiewicz University of Poznań ul. Umultowska 87, 61-614 Poznań, Poland. E-mail: [email protected]

Abstract: We present an infinitary logic ACT_ω in the form of a Gentzen-style sequent system, which is equivalent to the equational theory of *-continuous action lattices [9]. We prove the cut-elimination theorem for ACT_ω and, as a consequence, a theorem on the elimination of negative occurrences of *. This shows that ACT_ω is Π^0_1, whence, by a result of Buszkowski [1], it is Π^0_1 complete.

Keywords: Kleene algebra, action algebra, action lattice, cut-elimination, complexity

Journal: Fundamenta Informaticae, vol. 78, no. 2, pp. 295-309, 2007