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)

摘要： Eiter等人为语义网提出的回答集程序和描述逻辑相结合的描述逻辑程序，获得了本体上的非单调表达和推理能力。王以松等人证明了描述逻辑程序的完备化和环公式可以精确刻画描述逻辑程序的回答集。在此基础上，进一步证明了若完备化公式的模型不是回答集则一定存在终止环公式反例，它们是多项式时间可计算的。设计并实现了借助SAT求解器MiniSAT以及描述逻辑推理机RacerPro计算描述逻辑强回答集的原型DLP_SAT。实验结果表明，该原型能有效地计算一些熟知的描述逻辑程序的强回答集。

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