A Dynamic Description Logic for Semantic Web Service

This paper presents a dynamic description logic and a sound and complete tableau-based satisfiability-checking algorithm for it. This logic is a combination of a typical action theory and the description logic ALCO@, with a feature that actions are treated as citizens. On the one hand, actions are represented over ontologies expressed in description logic; On the other hand, actions can be used as modal operators for the construction of concepts. Therefore, not only actions but also concepts with dynamic meanings can be described. Furthermore, actions can also be used as modal operators for the construction of formulas, so that many reasoning tasks on actions and concepts can be realized with the help of the satisfiability-checking algorithm for formulas. These properties make this logic more capable for the semantic web service.