Logic-based approaches to AI have the advantage that their behavior can in principle be explained with the help of proofs of the computed consequences. For ontologies based on Description Logic (DL), we have put this advantage into practice by showing how proofs for consequences derived by DL reasoners can be computed and displayed in a user-friendly way. However, these methods are insufficient in applications where also numerical reasoning is relevant. The present paper considers proofs for DLs extended with concrete domains (CDs) based on the rational numbers, which leave reasoning tractable if integrated into the lightweight DL $\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$. Since no implemented DL reasoner supports these CDs, we first develop reasoning procedures for them, and show how they can be combined with reasoning approaches for pure DLs, both for $\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$ and the more expressive DL $\mathcal{ALC}$. These procedures are designed such that it is easy to extract proofs from them. We show how the extracted CD proofs can be combined with proofs on the DL side into integrated proofs that explain both the DL and the CD reasoning.

翻译：基于逻辑的AI方法具有优势，其行为原则上可通过计算所得结论的证明进行解释。针对基于描述逻辑（DL）的本体，我们已通过实践验证该优势，展示了如何计算DL推理机推导结论的证明并以用户友好方式呈现。然而，在涉及数值推理的应用场景中，现有方法存在不足。本文探讨面向扩展了有理数具体域（CD）的DL证明方法——该扩展若集成至轻量级DL $\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$中，可保持推理可解性。鉴于尚无已实现的DL推理机支持此类CD，我们首先为其开发推理程序，并展示如何将之与纯DL推理方法相结合（涵盖$\mathcal{E}\hspace{-0.1em}\mathcal{L}_\bot$及更具表达力的DL $\mathcal{ALC}$）。这些程序的设计便于从中提取证明。我们进一步阐明如何将提取的CD证明与DL侧证明整合为统一证明，从而同时解释DL推理与CD推理过程。