The use of description logics as one of the primary logical languages for knowledge representation on the Web has created new challenges with respect to reasoning in these logics. In order to support the vision of a semantic web of interrelated ontologies, reasoning procedures have to be highly scalable and able to deal with physically distributed knowledge models. A natural way of addressing these problems is to rely on distributed inference procedures that can distribute the load between different solvers, thus reducing potential bottlenecks both in terms of memory and computation time. In this paper, we propose a distributed resolution approach that solves the problem by local resolution and propagation of derived axioms between different reasoners. The method is complete for first order logic, terminates for ALC ontologies and avoids duplication of axioms and inferences. The work can be seen as a building block for a large scale distributed reasoning infrastructure for the semantic web as envisioned in recent activities such as the Large Knowledge Collider (LarKC) project.
展开▼
