A New Mapping from ALCI to ALC
A New Mapping from ALCI to ALC
复制标题
从 ALCI 到 ALC 的新映射
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Jiewen Wu
中科院分区：
文献类型：
--
作者：
Yu Ding;Volker Haarslev;Jiewen Wu
众所周知，[Sch 91]给出了描述逻辑（DL）、命题模态逻辑（ML）和命题动态逻辑（PDL）的对应理论，并在同一篇文章中给出了具有相反角色的描述逻辑的公理系统。Schild的论文涵盖了本文所要讨论的内容，尽管他的论文没有明确提到名词和表达角色。另一方面，即使对于完整的PDL（ALCIreg），也已知消除匡威程序（DL中的逆角色）的约简;从匡威PDL到PDL的原始约简在[Gia 96]中。此外，文[GM 00]给出了求解匡威PDL的直接表格法，并对匡威程序的消除作了进一步的讨论。除了分级模式外，[Gia 96]中指出，以前的还原技术也适用于名词。本文对[Gia 96]中的一些观点作了较好的评述。这里提出的映射过程是基于一个简单的想法，即捕获由使用反向角色引起的可能的反向传播。这个过程包括三个步骤，标记，记录，极化，下面介绍。概念表达式/公式被假定为否定范数形式（NNF）。为了简单起见，存在性约束和普遍约束在某处被称为模态约束。关于描述逻辑（DL）的一般背景知识，我们参考[BCM 03]。
It is well known that a correspondence theory for description logics (DLs), propositional modal logics (MLs) and propositional dynamic logics (PDLs) was given in [Sch91] and that an axiomatic system for a description logic with inverse roles was presented in the same paper. Schild’s paper covers what is to be discussed in this paper although his paper did not mention nominals as well as expressive roles explicitly. On the other hand, reductions to eliminate converse programs (inverse roles in DLs) are known even for full PDL (ALCIreg); the original reduction from converse PDL to PDL was in [Gia96]. Moreover, a direct tableaux method for converse PDL and further discussions on the elimination of converse programs were given in [GM00]. Besides graded modalities, it was pointed out in [Gia96] that the previous reduction technique is also applicable to nominals. This paper shares some viewpoints well made in [Gia96]. The proposed mapping process here is based on the simple idea to capture possible backpropagation caused by the use of inverse roles. This process consists of three steps, tagging, recording, polarisation, which are introduced below. Concept expressions/formulae are assumed to be in negation norm form (NNF). For simplicity, existential restrictions and universal restrictions are called modal constraints somewhere. We refer to [BCM03] for usual background knowledge on description logics (DLs).