本体理由探求是本体研究领域中的重要推理任务之一。面对实际应用中常见的大规模轻量级本体,研究学者认为可以通过将本体分类过程编码为命题逻辑下的Horn子句的方式,把本体理由探求问题转化为求解命题逻辑公式下的最小不可满足子句集合(Minimal Unsatisfiable Set,MUS)问题。由于现有的基于SAT的本体理由求解方法在不同方面都存在限制,考虑到轻量级本体具有语言复杂度低、规模大的特点,有专家学者提出近似求解的思想,即在确定精确的MUS之前预先求得一个或多个近似的MUS。基于以上分析,本文提出了一种基于近似核方法的本体理由求解策略,该方法适用于求解关于大规模轻量级本体以及特定蕴含关系的理由。相关研究表明,当命题逻辑公式的规模较大时,利用局部搜索(Local Search,LS)算法可以更好地从不可满足的公式中提取出近似的MUS,即能够使局部搜索算法体现出更好的性能。本文具体工作内容如下:(1)利用模块化方法缩小Horn编码的规模。轻量级本体中的概念和公理基数较大,通过编码生成的子句集合规模更大,因此直接在子句集上使用局部搜索技术是不现实的也是不可行的。选择函数是基于特定蕴含关系与SAT实例之间的文字相关性进行子句的选择。利用基于语义的选择函数能够筛选出与特定蕴含关系无关的子句并将其删除,保留与蕴含关系存在语义相关的子句。用于SAT实例上的模块化方法能够有效地减小编码生成的子句集合的规模。(2)提出基于局部搜索方法的本体理由近似核探求策略。直接利用黑盒法或白盒法在大规模轻量级本体上进行本体理由求解会造成时间和资源的浪费。利用近似求解的思想能够实现预先选择出一个基于本体和特定蕴含关系的不可满足子句的子集合,再根据求解精确本体理由的方法从中提取理由。由于局部搜素策略对于子句的规模和类型没有特殊要求,因此基于局部搜索策略的近似核方法打破了以往近似求解方法存在的仅适用于某些特定类型的子句、仅适用于小规模的SAT实例等方面的限制。实验证明,近似核策略与已有的(?)SAT相比,在GO和NCI本体上求解理由的时间平均减少69%左右。(3)在近似核基础上,利用破坏法、构造法以及基于SAT的分治法三种策略在近似核基础上构建本体理由的精确求解过程。其中,破坏法是从近似核中迭代删除子句,构造法是将子句迭代插入到MUS中,基于SAT的分治法能够实现一次性删除多个子句。在上述三种方法的求解过程中,利用基于局部搜索策略判定SAT实例的可满足性。通过算法结构及计算复杂度的对比分析得出,基于SAT的分治法更适于本体理由的精确求解。本文实验结果表明,利用基于Horn编码的模块化方法能够将子句集的规模减小85%左右。基于近似核的本体理由探求方法适用于大规模的本体实例,实验效果明显优于(?)SAT,本体规模与求解时间呈近似线性关系。利用基于SAT的分治法能够计算出大规模轻量级本体的精确理由。