Enumerating Justifications using Resolution
Enumerating Justifications using Resolution
复制标题
DOI：
10.1007/978-3-319-94205-6_40
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
Yevgeny Kazakov;P. Skocovsky
中科院分区：
文献类型：
--
作者：
Yevgeny Kazakov;P. Skocovsky
如果一个结论来自一组公理，那么它的正当性就是蕴涵成立的公理的一个极小子集。牵连可以有几个理由。这样的理由通常用于调试描述逻辑本体论中的不正确蕴涵。最近，已经提出了一些基于SAT的方法，它们可以列举轻量级本体语言中蕴涵的所有理由，例如。这些方法的工作方式是对命题Horn逻辑中的推理进行编码，并使用SAT解算器找到与理由相对应的最小模型。在这篇文章中，我们提出了一种新的理由枚举过程，它使用带有答案文字的归结而不是SAT求解器。与基于SAT的方法相比，我们的过程可以按照任何用户定义的顺序枚举证明，从而扩展了集合包含关系。该过程易于实现，并且与解析一样，可以使用排序和选择策略进行参数化。我们已经在一个新的基于Java的证明实用程序库Puli中实现了这个过程，并在流行本体上对我们的过程和基于SAT的工具进行了(几种策略)的经验比较。实验表明，我们的过程提供了与那些高度优化的工具相当的、而且往往更好的性能。例如，使用其中一种策略，我们第一次能够计算出最大的常用医学本体之一Snowed CT中所有相关概念包含的所有理由。
If a conclusion follows from a set of axioms, then its justification is a minimal subset of axioms for which the entailment holds. An entailment can have several justifications. Such justifications are commonly used for the purpose of debugging of incorrect entailments in Description Logic ontologies. Recently a number of SAT-based methods have been proposed that can enumerate all justifications for entailments in light-weight ontologies languages, such as. These methods work by encodinginferences in propositional Horn logic, and finding minimal models that correspond to justifications using SAT solvers. In this paper, we propose a new procedure for enumeration of justifications that uses resolution with answer literals instead of SAT solvers. In comparison to SAT-based methods, our procedure can enumerate justifications in any user-defined order that extends the set inclusion relation. The procedure is easy to implement and, like resolution, can be parametrized with ordering and selection strategies. We have implemented this procedure in PULi—a new Java-based Proof Utility Library, and performed an empirical comparison of (several strategies of) our procedure and SAT-based tools on popularontologies. The experiments show that our procedure provides a comparable, and often better performance than those highly optimized tools. For example, using one of the strategies, we were able for the first time to compute all justifications for all entailed concept subsumptions in one of the largest commonly used medical ontology Snomed CT.