描述逻辑和具体领域推理的证明合并（技术报告）
摘要：基于逻辑的人工智能方法具有一个优势，即它们的行为原则上可以通过计算出的结果的证明来解释。对于基于描述逻辑（DL）的本体论，我们已经将这个优势应用到实践中，通过展示如何计算和显示由DL推理程序推导的结果的证明，以用户友好的方式。然而，在涉及数值推理的应用场景中，这些方法是不足够的。本文关注基于有理数的具体域（CDs）扩展的DL的证明，如果集成到轻量级DL $mathcal{E}hspace{-0.1em}mathcal{L}\_ot$ 中，可以使推理可行。由于没有实现的DL推理程序支持这些CDs，我们首先为它们开发推理过程，并展示如何将它们与纯DL的推理方法相结合，包括$mathcal{E}hspace{-0.1em}mathcal{L}\_ot$和更有表现力的DL $mathcal{ALC}$。这些过程的设计使得从中提取证明非常容易。我们展示了如何将提取的CD证明与DL证明结合成综合证明，同时解释DL和CD推理。
作者：Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann and Alisa Kovtunova
论文ID：2308.03705
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-08