The product of converse PDL and polymodal K
Frank Wolter · Journal of Logic and Computation · 2000
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.