近年来,轻量级描述逻辑语言逐渐吸引了专家学者们的注意,这种表达能力较弱但是复杂性低的语言更适合构建大型本体。随着本体规模的不断增大,在本体构建过程中不可避免会产生的各种逻辑冲突。这些冲突如果未被及时修正,会影响本体工程或知识工程的一系列下游应用。为了高效调试生成语义正确的大规模本体,通常使用公理定位方法探索本体中的缺陷并计算逻辑结果的隐藏理由。公理定位（Axiom pinpointing,AP）是描述逻辑本体中的一项重要的推理任务,它的目的是在本体中找到给定逻辑结论的理由,即最小公理集合（Minimal axiom set,Min A）。与传统公理定位方法相比,近年来提出的基于Horn编码的定位方法更为高效。它将本体的分类（classification）过程编码为命题逻辑Horn公式,即Horn定位公式,并通过计算Horn定位公式中的最小不可满足子集（minimal unsatisfiable subset,MUS）来获取给定描述逻辑逻辑结论的Min A。得益于SAT求解技术的快速发展,针对求解单一理由的Horn编码公理定位算法和实现工具已趋于完善和高效,但是对于枚举逻辑结论全部理由的研究有待进一步发展。面对轻量级描述逻辑本体中全部理由的枚举问题,本文具体工作如下:1)将最小不可满足核的枚举框架——种子收缩（seed-shrink）枚举框架应用于描述逻辑本体推理中,提出了基于种子收缩的本体理由枚举框架。该框架首先构造本体的Horn编码,迭代获取Horn定位公式的子公式作为种子,随后判定种子的可满足性,最终经过收缩不可满足的种子获得全部Min A。2)在种子收缩枚举框架下,改进本体理由枚举算法。通常情况下,种子收缩过程会优先枚举较大的种子,但计算成本较高。针对该问题,本文提出了两种优化策略:递归法和复制法。递归法在每次迭代中逐步缩小搜索空间的范围,从中可以获取较小的种子。在当前递归层次没有新种子时,回溯至上一层继续搜索。而复制法在迭代中使用已知Min A结果逐步扩展搜索空间的范围,并且运用归结原理从已知结果构造新的不可满足种子,代替了部分可满足性判定操作。以上的两种改进算法从不同的角度限制了获取种子的大小,减少了收缩种子的代价。经过实验对比,递归法和复制法都在一定程度上加速了枚举进程。另外,复制法构造不可满足种子的操作减少了种子可满足性判定的频率,使得复制法的优化效果更明显。3)除了将递归和复制策略用于优化本体理由的枚举,本文还针对Horn定位公式进行SAT求解器进行参数调优,进一步提升枚举过程的整体效率。具体来说:本文根据Horn公式编码的结构与特点修改了可满足判定算法中的重启策略、学习子句管理方法以及VSIDS分支启发式的衰减参数,使得新的求解器更适合于Horn定位公式种子的可满足性判定。实验结果表明,本文定制的Horn定位公式求解器普遍提高了种子可满足性判定效率,进一步加速了基于种子收缩枚举的本体理由枚举。本文使用生物医学本体Gene、Galen、NCI以及超大型本体Snomed-CT进行了实验。实验结果表明基于种子收缩的Min A枚举算法能够有效计算给定推论的全部理由,并且求解效率上优于算法EL2MUS、SATPin等算法。其中,使用了定制SAT求解器的复制法在所有算法中性能最优。