论文部分内容阅读
利用非循环定义的概念可展开的特性,提出一个基于子句重构的增强Tableau算法.采用最简洁的概念合取子句代替原来的子概念集对完整树/图上的结点进行标记,并设计一组推理规则以构建这样的完整树/图,从而消除传统Tableau算法中的∩-规则、∪-规则所带来的概念描述重复.因而在非循环定义概念可满足性判定问题上,空间性能有明显提高.此外,虽然文中只提供针对SI语言的规则和证明,可是这种处理思路同样适用于其它描述逻辑语言,因而具有一定的推广价值.
In this paper, we propose an enhanced Tableau algorithm based on clause refactorings by using the concept of non-cyclical definition.Using the simplest concept conjunction clauses instead of the original sub-concept sets to mark the nodes on the complete tree / graph, And design a set of inference rules to construct such a complete tree / graph, thereby eliminating the recurrence of concept descriptions brought by the ∩-rule and ∪-rule in the traditional Tableau algorithm.Therefore, on the issue of satisfiability determination of the concept of non-cyclic definitions, In addition, although the text only provides rules and certificates for SI language, but this approach also applies to other description logic language, which has a certain promotional value.