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

• Autorzy: Palka E.
• Języki publikacji: EN

Abstrakty

EN

We present an infinitary logic ACTw 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 ACTw and, as a consequence, a theorem on the elimination of negative occurrences of *. This shows that ACTw is P01, whence, by a result of Buszkowski [1], it is P01-complete.

Słowa kluczowe

EN

Kleene algebras; action algebras; action lattice; cut-elimination; complexity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 78, nr 2
• Strony: 295--309
• Opis fizyczny: bibliogr. 10 poz.

Twórcy

autor

Palka E.

• Faculty of Mathematics and Computer Science, Adam Mickiewicz University, Umultowska 87, 61-614 Poznań, Poland,

Bibliografia

• [1] Buszkowski, W.: On Action Logic, manuscript, to appear in: Journal of Logic and Computation, www.staff.amu.edu.pl/ buszko/actlog2.pdf
• [2] Jipsen, P.: From Semirings to Residuated Kleene Algebras, Studia Logica, 76, 2004, 291-303.
• [3] Kozen, D.: On Kleene algebras and closed semirings, in: Proc. MFCS 1990, Lecture Notes in Comp. Science 452, 1990, 26-47.
• [4] Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events, Information and Computation 110:2, 1994, 366-390.
• [5] Kozen, D.: On Action Algebras, manuscript, in: Logic and the Flow of Information Amsterdam, 1991.
• [6] Lambek, J.: The mathematics of sentence structure, The American Mathematical Monthly 65, 1958, 154-170.
• [7] Ono, H.: Semantics for Substructural Logics, in: Substructural Logics, (Schroeder-Heister, P., Došen, K., eds.), Clarendon Press, Oxford, 1993, 259-291.
• [8] Palka, E.: On Finite Model Property of the Equational Theory of Kleene Algebras, Fundamenta Informaticae 68.3, 2005, 221-230.
• [9] Pratt V.: Action Logic and Pure Induction, in: Logics in AI. Proc. of JELIA'90, Lecture Notes in Artif. Inteligence 478, 1991, 97-120.
• [10] Redko, V.N.: On defining relations for the algebra of regular events, Ukrain. Mat. Z. 16, 1964, 120-126. In Russian.