基于Tableau算法的本体模型验证方法研究＊

兰 天 程继红

（海军航空工程学院科研部 烟台 264001）

1 引言

本体模型的检验是以描述逻辑为基础的，利用描述逻辑来实现术语及其约束关系的形式化描述。描述逻辑是人工智能领域研究的分支，是基于对象的形式化知识的表示方法，它能依据提供的构造器，在简单的概念和关系上构造出复杂的概念和关系。描述逻辑的知识库有两部分组成，即∑＝〈Tbox，Abox〉，Tbox是有关概念和关系的蕴涵断言集合，描述概念和关系的一般属性；Abox是有关个体的实例断言集合，断言一个个体是某个概念的实例，或者两个个体之间存在某种关系。因此模型的检验主要包括Tbox术语检验和Abox实例检验。

2 本体模型的一致性检验

2.1 Tbox术语检验推理

给定模型 M＝M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E为两个术语，则Tbox术语检验包括4种：

1）术语的可满足性检验：如果存在Tc与Rc的一个共同模型I满足DI≠Ø，则称D关于Tc与Rc是可满足的，否则称D关于Tc与Rc是不可满足的。

术语的可满足性用于评价术语公式对于术语集是否有意义。

2）术语的包含性检验：如果对任意一个Tc与Rc共同的模型I有DI⊆EI，则称Tc与Rc蕴含着E包含D，记为（Tc＋Rc）╞D⊆E。

包含性检验用于评价本体中术语之间的包含关系，可以用来建立术语集的层次结构。

3）术语的等价性检验：如果对任意一个Tc与Rc共有的模型I有DI＝EI，则称Tc与Rc蕴含着E包含D，记为（Tc＋Rc）╞D≡E。

等价性检验用于评价两个术语是否具有相同的实例集。

4）术语的非交性检验：如果对任意一个Tc与Rc共有的模型I有DI∩EI＝Ø，则称Tc与Rc蕴含着D与E非交，记为（Tc＋Rc）╞D⊆﹁E。

非交性检验用于判断两个术语是否具有相同的实例。……