发表机构
TU Dresden（德累斯顿工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对知识图谱中规则推理机重写本体规则后无法从证明树生成原始规则解释的问题，研究从重写规则的蕴含证明构造原始规则证明的方法，确定其计算复杂度并识别两种实用证明变换语言。
AI 中文摘要
Datalog规则常被用于定义知识图谱上的本体。规则推理机通常会重写这类本体的规则，以将其优化为可更高效评估的形式。这些变换会保留蕴含的事实，但不保留底层推导的结构。重写规则下的证明树可解释某一事实成立的原因，但难以直接生成基于原始规则的解释。我们研究从重写规则下的蕴含证明构造原始规则下证明的问题：确定了其计算复杂度，并识别出两种用于指定证明变换的实用相关语言。
英文摘要
Datalog rules are often used to define ontologies over Knowledge Graphs. Rule reasoners routinely optimise such ontologies by rewriting their rules into a form that can be evaluated more efficiently. These transformations preserve the entailed facts, but not the structure of the underlying derivations. A proof tree under the rewritten rules explains why a fact holds, but does not readily yield an explanation in terms of the original rules. We study the problem of constructing, from a proof of entailment under the rewritten rules, a proof under the original ones: we establish its computational complexity and identify two practically relevant languages for specifying proof transformations.
