CAJ | 학술논문

由于目前tableau算法在判断概念可满足性时会产生大量的描述重复(因而浪费了很多空间),针对描述逻辑语言ALCN提出了一种基于子句重构的tableau增强方式.该增强方式对概念描述先构建一个析取范式,并只保留其中的一个合取子句,然后用这个获得的最简的概念合取子句去取代传统tableau算法构建的完整树的结点标记中的子概念集(这个过程根据需要可重复多次).由于避免了传统tablcau算法因∩-,∪-规则所带来的大量的概念描述重复,这种增强方式在空间性能上有了非常大的改善.通过例子示范了这种增强方式的运用及其在空间性能上的改善程度.结果表明,这种改善是相当明显的.
유우목전tableau산법재판단개념가만족성시회산생대량적묘술중복(인이낭비료흔다공간),침대묘술라집어언ALCN제출료일충기우자구중구적tableau증강방식.해증강방식대개념묘술선구건일개석취범식,병지보류기중적일개합취자구,연후용저개획득적최간적개념합취자구거취대전통tableau산법구건적완정수적결점표기중적자개념집(저개과정근거수요가중복다차).유우피면료전통tablcau산법인∩-,∪-규칙소대래적대량적개념묘술중복,저충증강방식재공간성능상유료비상대적개선.통과례자시범료저충증강방식적운용급기재공간성능상적개선정도.결과표명,저충개선시상당명현적.
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.