局部性及其在 $\mathcal{EL}$ 及其部分扩展中的包含测试与插值应用

在本文中，我们展示了轻量级描述逻辑（如 $\mathcal{EL}$ 和 $\mathcal{EL}^+$）中的包含问题可以表示为具有单调算子的半格类中的统一字问题。我们利用此类代数中高效局部推理的可能性，获得了 $\mathcal{EL}$、$\mathcal{EL}^+$ 及其扩展中 CBox 包含的统一 PTIME 判定过程。这些局部性考虑使我们能够提出一个新的（可能是多排序的）逻辑族，该逻辑族将 $\mathcal{EL}$ 和 $\mathcal{EL}^+$ 扩展了 $n$ 元角色和/或数值域。作为副产品，这使我们能够证明 ${\cal EL}$ 和 ${\cal EL}^+$ 的代数模型具有基插值性，从而证明 ${\cal EL}$、${\cal EL}^+$ 以及本文研究的它们的扩展具有插值性。我们还展示了如何将这些思想用于描述逻辑 $\mathcal{EL}^{++}$。