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