εL~+是描述当前流行的大规模医学本体的一种轻量级描述逻辑语言,它的广泛使用引起了研究者对该语言下推理问题的研究兴趣。本文致力于解决描述逻辑εL~+中理由的抽取,实现对公理的快速定位,从而找到蕴含目标公理的最小公理集。黑盒法是抽取理由的主要方法,通常需要进行多次蕴含测试,因为其核心思想是将本体缩减为蕴含目标公理的理由,所以可以认为是破坏性的抽取过程。在这种情况下,本文提出一种检测本体中关键公理的构造方法,而不是通过传统的从本体中删除无关公理的破坏性方法。具体研究内容如下:(1)本文分析了叶提出的理由抽取算法,并指出该方法实际是一种构造性的抽取方法。此外,我们分析了算法的复杂度,令m表示本体中的公理数,k表示理由中的公理数,假设向一个空本体集中添加公理要添加m次才能确认蕴含目标公理,再将得到的关键公理添加到理由中,最多添加k次,那么需要对本体推理机进行O(m~*k)次调用。(2)我们在基础的构造性理由抽取框架下,开发了一种轻量级大规模本体下的构造性理由抽取算法。该算法以理由抽取问题转化为对命题公式的极小不可满足子公式(MUS)的提取问题为基础工作,提出以下优化策略:(i)首先是子句集求精和冗余去除技术。子句集求精等效于对大型命题公式的MUS抽取的预处理技术,以减少对SAT求解器的调用。而冗余去除技术能与子句集求精共同使用但不是立即的,而是需要一个简单测试,以决定何时将不可满足的超集用作下次循环中作为有效的CNF公式。(ii)其次是模型轮转技术。模型轮转可以通过对模型赋值中的变量迭代取反的方法,不断检测出命题公式中的关键子句,以构造MUS。从而减少SAT求解器的调用,加速对MUS的抽取。实验证明,构造性的理由抽取方法通过检测关键公理,可以避免检测无关公理,在效率和性能方面都优于传统黑盒法。而且在轻量级大规模本体下,构造性的理由抽取方法通过模型轮转的策略进一步减少了检测次数。