论文部分内容阅读
描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础。描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握ALC中的Tableau算法是理解各种描述逻辑中可判定性的基础。对ALC中的Tableau算法进行详细阐述,并对其关键的几个性质:可终止性、完备性和判定性给出了证明,为研究SHOIN(D)中的Tableau算法及性质奠定了基础。