Completion Graph Caching for Expressive Description Logics
Completion Graph Caching for Expressive Description Logics
复制标题
表达描述逻辑的完成图缓存
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Thorsten Liebig
中科院分区：
文献类型：
--
作者：
Andreas Steigmiller;Birte Glimm;Thorsten Liebig
在非常有表现力的描述逻辑(DLS)中进行推理通常是困难的，因为非决定论，例如来自析取或基数限制的非决定论，需要逐个案例分析，并且由于名词性的原因，内涵(TBox)和外延(ABox)知识之间的严格分离是不可能的。当前最先进的SROIQ推理器通常基于(超)Tableau算法，其中诸如分类等更高级别的推理任务被简化为可能的许多一致性测试。对于大的ABox和更具表现力的DL，推理很容易变得不可行，因为在每次测试中都必须考虑ABox。对于表现力较弱的DLS，已经提出了优化方案，允许仅考虑ABox的一部分来检查个人是否是特定概念的实例[22，23]。然而，目前还不清楚这些优化如何扩展到SROIQ。此外，基于划分和模块化的方法需要对知识库中的概念、角色和个体进行语法预分析，这对于更具表现力的DL来说可能是相当昂贵的，并且由于静态分析，仅支持具有特定概念的查询。重写公理以便改进ABox推理也存在这样的风险，即这会对ABox推理可能不相关或不太相关的其他推理任务产生负面影响。另一种可能性是缓存在初始一致性检查期间由Tableau算法构建的完成图。在后续测试中重用缓存的完成图(部分)减少了必须为ABox的个体重新派生的结果的数量。然而，基于这一思想的现有方法(例如，[17])不太适合处理非决定论。由于缓存和重新使用非确定性派生事实很容易导致不可靠的后果，因此非确定性派生事实通常被简单地丢弃，并在必要时重新派生。我们解决了这一问题，并提出了一种技术，允许识别可以安全地重用的不确定事实。该方法基于一组可以在本地检查的条件，因此允许有效地逐步识别个人，对于这些个人，在后续测试中必须重新考虑不确定性后果。所提出的技术可以直接集成到现有的基于表格的推理系统中，而无需进行重大调整，并减少了ABox结果潜在相关的所有任务的推理工作量。此外，
Reasoning in very expressive Description Logics (DLs) such as SROIQ is often hard since non-determinism, e.g., from disjunctions or cardinality restrictions, requires a case-by-case analysis and since a strict separation between intensional (TBox) and extensional (ABox) knowledge is not possible due to nominals. Current state-of-the-art reasoners for SROIQ are typically based on (hyper-)tableau algorithms, where higher level reasoning tasks such as classification are reduced to possibly many consistency tests. For large ABoxes and more expressive DLs, reasoning then easily becomes infeasible since the ABox has to be considered in each test. For less expressive DLs, optimisations have been proposed that allow for considering only parts of the ABox for checking whether an individual is an instance of a specific concept [22,23]. It is, however, not clear how these optimisations can be extended to SROIQ. Furthermore, approaches based on partitioning and modularisation require a syntactic pre-analysis of the concepts, roles, and individuals in a KB, which can be quite costly for more expressive DLs and, due to the static analysis, only queries with specific concepts are supported. Rewriting axioms such that ABox reasoning is improved also carries the risk that this negatively influences other reasoning tasks for which ABox reasoning is potentially not or less relevant. Another possibility is the caching of the completion graph that is built by the tableau algorithm during the initial consistency check. The re-use of (parts of) the cached completion graph in subsequent tests reduces the number of consequences that have to be re-derived for the individuals of the ABox. Existing approaches based on this idea (e.g., [17]) are, however, not very suitable for handling non-determinism. Since caching and re-using non-deterministically derived facts can easily cause unsound consequences, the non-deterministically derived facts are usually simply discarded and re-derived if necessary. We address this and present a technique that allows for identifying nondeterministic facts that can safely be re-used. The approach is based on a set of conditions that can be checked locally and, thus, allows for efficiently identifying individuals step-by-step for which non-deterministic consequences have to be re-considered in subsequent tests. The presented technique can directly be integrated into existing tableaubased reasoning systems without significant adaptations and reduces reasoning effort for all tasks for which consequences from the ABox are potentially relevant. Moreover,
DOI：
10.1007/s10817-014-9305-1
发表时间：
2014-10-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Glimm, Birte;Horrocks, Ian;Wang, Zhe
通讯作者：
Wang, Zhe