The product of converse PDL and polymodal K

10 years 11 months ago
The product of converse PDL and polymodal K
The product of two modal logics L1 and L2 is the modal logic determined by the class of frames of the form FG such that F and G validate L1 and L2, respectively. This paper proves the decidability of the product of converse PDL and polymodal K. Decidability results for products of modal logics of knowledge as well as temporal logics and polymodal K are discussed. All those products form rather expressive but still decidable fragments of modal predicate logics. Based on the equivalence of polymodal K and the description logic ALC we shall discuss the obtained fragments, extend the expressive power a bit, and compare them with other modal description logics.
Frank Wolter
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2000
Authors Frank Wolter
Comments (0)