$\mathcal{EL}$ 证明的形状：三种计算方法的故事（扩展版）
计算机科学中的逻辑
2025-07-30 v1
摘要
基于后果的推理可用于构造解释描述逻辑(DL)本体条款的证明。在文献中，针对家族DL的多种后果计算方法可找到，每种方法产生不同形状的证明。本文研究三种此类计算方法及其在基于OWL Reasoner Evaluation基准测试中产生的证明。这些计算方法通过转化为带分层否定的本体规则实现，此方法已被证明对ELK理由器有效。随后，我们使用规则引擎NEMO评估这些规则并获取规则执行轨迹。通过将这些轨迹转换回DL证明，我们在反映不同复杂度方面性质的多项指标上进行比较。
引用
@article{arxiv.2507.21851,
title = {The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)},
author = {Christian Alrabbaa and Stefan Borgwardt and Philipp Herrmann and Markus Krötzsch},
journal= {arXiv preprint arXiv:2507.21851},
year = {2025}
}
备注
Extended version of a paper accepted at 38th International Workshop on Description Logics (DL 2025)