Properties and Distributed Tableaux Reasoning Algorithm for D3L(ccy)

As the distributed extension of traditional dynamic description logics(DDL), distributed dynamic description logics(D3L) enables reasoning with multiple heterogeneous DDL ontologies interconnected by directional semantic mapping. D3L captures the idea of importing and reusing knowledge between several ontologies. This idea combines well with the basic assumption of the distributed and dynamic systems such as the semantic Web and the heterogeneous information integration system. We find in the case when more than two ontologies are involved and bridge rules form chains, knowledge does not always propagate along chains of bridge rules even if we would expect it. Inspired by package-based description logics, we propose D3L(ccy) by imposing so called compositional consistency condition on domain relations in D3L interpretations. Under this semantics knowledge propagates along chains of bridge rules correctly. We research the properties and distributed Tableaux reasoning algorithm for D3L(ccy) systematically. We prove that D3L(ccy) satisfies the monotonicity property(D3L(ccy) is a monotonic logic), the directionality property(the effect of bridge rules is directional) and the restrained inconsistency propagation property(if some of the local ontologies is inconsistent, it does not necessarily pollute the whole distributed system). Furthermore we provide a distributed Tableaux reasoning algorithm which is sound and complete for deciding satisfiability of concepts in D3L(ccy). Compared with original one, the extended D3L provides more reasonable logic foundation for distributed and dynamic systems such as the Semantic Web and the information integration system.