Combining Proofs for Description Logic and Concrete Domain Reasoning (Technical Report)

TL;DR

This paper develops proof methods for combined Description Logic and concrete domain reasoning, enabling explanations that integrate numerical and logical reasoning in AI ontologies.

Contribution

It introduces reasoning procedures for DLs with concrete domains and shows how to combine their proofs with traditional DL proofs for integrated explanations.

Findings

Proof procedures for DLs with concrete domains are developed.

Integrated proofs combining DL and concrete domain reasoning are demonstrated.

The methods facilitate explainable AI with numerical and logical reasoning.

Abstract

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.