中文摘要：

由于目前tableau算法在判断概念可满足性时会产生大量的描述重复（因而浪费了很多空间）,针对描述逻辑语言ALCN提出了一种基于子句重构的tableau增强方式.该增强方式对概念描述先构建一个析取范式,并只保留其中的一个合取子句,然后用这个获得的最简的概念合取子句去取代传统tableau算法构建的完整树的结点标记中的子概念集（这个过程根据需要可重复多次）.由于避免了传统tableau算法因∩-,∪-规则所带来的大量的概念描述重复,这种增强方式在空间性能上有了非常大的改善.通过例子示范了这种增强方式的运用及其在空间性能上的改善程度.结果表明,这种改善是相当明显的.

英文摘要：

As the tableau algorithm would produce a lot of description overlaps when judging the satisfiabilities of concepts（thus wasting much space）,a clause-based enhancing mode designed for the language ALCN is proposed.This enhancing mode constructs a disjunctive normal form on concept expressions and keeps only one conjunctive clause,and then substitutes the obtained succinctest conjunctive clause for sub-concepts set in the labeling of nodes of a completion tree constructed by the tableau algorithm （such a process may be repeated as many times as needed）.Due to the avoidance of tremendous descriptions redundancies caused by applying ∩- and ∪-rules of the ordinary tableau algorithm,this mode greatly improves the spatial performance as a result.An example is given to demonstrate the application of this enhancing mode and its reduction in the cost of space. Results show that the improvement is very outstanding.