Satis ability problem in description logics with modal operators
Satis ability problem in description logics with modal operators
复制标题
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
F. Wolter;M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
F. Wolter;M. Zakharyaschev
本文考虑了在标准概念描述语言ALC中扩充各种模态算子，使之能应用于概念和公理。其主要目的是发展证明这种语言的萨蒂斯度问题的可判定性的方法，并将其应用于具有最重要的时态和认知算子的描述逻辑，从而获得这些逻辑的萨蒂斯度检查算法。我们讨论了可能世界的语义在恒定域假设下，证明了扩展域和变域假设都可以约化到它，并研究了具有任意恒定域和有限恒定域的模型.我们开始考虑的描述逻辑只有一个模态算子，然后证明了一个一般的转移定理，这使得它有可能提升所获得的结果到许多系统的多模态描述逻辑。
The paper considers the standard concept description language ALC augmented with various kinds of modal operators which can be applied to concepts and axioms. The main aim is to develop methods of proving decidability of the satis ability problem for this language and apply them to description logics with most important temporal and epistemic operators, thereby obtaining satis ability checking algorithms for these logics. We deal with the possible world semantics under the constant domain assumption and show that the expanding and varying domain assumptions are reducible to it. Models with both nite and arbitrary constant domains are investigated. We begin by considering description logics with only one modal operator and then prove a general transfer theorem which makes it possible to lift the obtained results to many systems of polymodal description logic.