Distributed Resolution for ALC

The use of Description Logic as the basis for Semantic Web Languages has led to new requirements with respect to scalable and nonstandard reasoning. In this paper, we address the problem of scalable reasoning by proposing a distributed, complete and terminating algorithm that decides satisfiability of terminologies in ALC. The algorithm is based on recent results on applying resolution to description logics. We show that the resolution procedure proposed by Tammet can be distributed amongst multiple resolution solvers by assigning unique sets of literals to individual solvers. This results provides the basis for a highly scalable reasoning infrastructure for Description logics.

• Type: Conference
• Year: 2008
• Where: DLOG
• Authors: Anne Schlicht, Heiner Stuckenschmidt
• Keywords: Automated Reasoning, Description Logics, DLOG 2008, Scalable Reasoning, Scalable Reasoning Infrastructure