关键词: 描述逻辑, 逻辑程序, 回答集, 环公式, 可满足性问题（SAT）

Abstract: Eiter et al. proposed an approach to combining answer set programs with description logics, called description logic program (DLP) for the semantic Web. It results in the non-monotonicity for the reasoning over ontology. Wang et al. showed that, together with the notion of loop formulas, the completion of a DLP can precisely capture the answer sets of DLP. Accordingly, this paper proves that there exist terminating loop formulas validating the models of the completion for a DLP that can be efficiently computed in polynomial time. Then, this paper presents a prototype DLP_SAT for computing strong answer sets of DLPs, which makes use of SAT solver MiniSAT and description logic reasoner RacerPro. The experimental results demonstrate that the prototype can efficiently compute the strong answer sets of some known DLPs.

Key words: description logic, logic program, answer set, loop formula, satisfiability (SAT)