描述逻辑程序系统的设计与实现

摘要：

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

关键词：描述逻辑、逻辑程序、回答集、环公式、可满足性问题(SAT)

分类号：TP181(自动化基础理论)

资助基金：The National Natural Science Foundation of China under Grant No.61370161;the Stadholder Funds for Outstanding Scientific and Technological Talent of Guizhou Province under Grant No.201262

在线出版日期：2014-03-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：338-344