Journal of Logic and Computation, Volume 10, Issue 2, pp. 223-251: Abstract.
The product of converse PDL and polymodal K
Institut für Informatik, Universität Leipzig, Augustus-Platz 10-11, 04109 Leipzig, Germany, E-mail: email@example.com
The product of two modal logics L1 and L2 is the modal logic determined by the class of frames of the form F x G 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 from 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 fragments obtained, extend the expressive power a bit, and compare them with other modal description logics.
Keywords: dynamic logic, modal logic, description logic, products, decidability