Tableau-based 算法的改进与有限步终止定理-陕西师范大学学报期刊社网站

陕西师范大学学报（自然科学版）

数学与计算机科学

Tableau-based 算法的改进与有限步终止定理

王国俊,李璧镜

(陕西师范大学数学与信息科学学院, 陕西西安 710062)

王国俊, 男, 教授,博士研究生导师, 从事不确定性推理方面的研究.

摘要:

对原有的tableau-based算法进行了简化和改进,提出了标准tableau-based算法,它在保证原有算法思想的基础上删除了每次变换后所产生的累赘部分,同时不再限制运算的顺序.基于这个新算法,证明了ALCN语言中Abox的相容性可通过标准tableau-based算法在有限步之内判定.

关键词：

描述逻辑; Abox; tableau-based算法; 标准tableau-based 算法; 有限步终止定理

收稿日期：

2008-03-15

中图分类号：

O142

文献标识码：

文章编号：

1672-4291(2008)06-0001-04

基金项目：

国家自然科学基金资助项目(10771129)

Doi:

Improvement of tableau-based algorithm and finite step halting theorem

WANG Guo-jun, LI Bi-jing

(College of Mathematics and Information Science, Shaanxi Normal University, Xi′an 710062, Shaanxi, China)

Abstract:

The tableau-based algorithm for consistency checking of Aboxes is simplified and improved.The proposed standard tableau-based algorithm not only deletes the redundant part after each rule, but also gives up the restriction on the order of transformation rules. So this is a simplification and an improvement of the algorithm, and the finite step halting theorem for checking consistency of ALCN Aboxes is obtained therefrom.

KeyWords:

description logic; Abox; tableau-baesd algorithm; standard tableau-based algorithm; finite step halting theorem