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

2011-06-06程继红

舰船电子工程 2011年10期

兰天程继红

（海军航空工程学院科研部烟台 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。

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

可满足性问题是描述逻辑推理过程的一个核心问题，其他四种检验都可以转换成可满足性检验：

命题1 给定模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，D和E为两个术语，可以得到以下转换：

1）（Tc＋Rc）╞D⊆E，当且仅当，D∩﹁E关于Tc与Rc是不可满足的；

2）（Tc＋Rc）╞D≡E，当且仅当，D∩﹁E与﹁D∩E关于Tc与Rc是不可满足的；

3）（Tc＋Rc）╞D⊆﹁E，当且仅当，D∩E关于Tc与Rc是不可满足的。

2.2 Abox实例检验推理

Abox实例检验主要包括实例声明的一致性检验和实例声明集的一致性检验。

实例声明的一致性检验：给定本体模型M＝〈Ta，Tc，Pd，Rc，Xd〉，若存在解释I是实例声明 C（a）的一个模型，则称C（a）是一致的。若I是C（a）的一个模型，又是Tc与Rc的一个模型，则称C（a）关于Tc与Rc是一致的。若I是Xd的一个模型，则称Xd是一致的。若I是Xd的一个模型，又是Tc与Rc的一个模型，则称Xd关于Tc与Rc是一致的。

实例声明的一致性检验用于检验实例的声明是否存在矛盾。

实例声明集的一致性检验：给定本体模型M＝〈Ta，Tc，Pd，Rc，Xd〉，如果 Xd的每一个模型I都满足实例声明C（a），则称Xd蕴含着C（a），记为Xd╞C（a）。

命题2 给定本体模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，Xd╞C（a），当且仅当，Xd∪｛﹁C（a）｝是不一致的。

因此，实例声明的一致性检验又可以转换为实例声明集的一致性检验。

2.3 术语检验与实例检验的转换关系

命题3 给定本体模型 M＝〈Ta，Tc，Pd，Rc，Xd〉，C关于Tc与Rc是可满足的，当且仅当，存在个体a，使得实例声明集｛C（a）｝关于Tc与Rc是一致的。

由此命题可以得出术语检验与实例检验两者不是相互独立的，而是存在着紧密联系的，实例声明集的一致性检验与术语的可满足性检验是可以相互转换的。由命题1、命题2、命题3可知，术语的包含性、等价性、非交性检验以及实例声明的一致性检验和实例声明集的一致性检验均可约简为可满足性检验。因此，本体模型的一致性检验就可以简化为术语的可满足性检验。

3 可满足性检验

Tableau算法最早是由Schmidt-Schau和Smolka为检验ALC概念的可满足性而提出［1］，主要用于在逻辑系统中对概念的定义以及概念间的关系进行可满足性测试，是描述逻辑推理系统的核心算法。该算法的基本思路是：通过公式来逐渐构建模型，通过自顶向下的方式来分解公式。此过程一直持续，直到找完所有可能公式。目的是为了证明没有找到不可满足公式的模型。

表1 本体模型可满足性检验的算法规则

借鉴Tableau算法的思想，本文提出了一个本体模型术语可满足性检验的基本思路：给定一个术语描述C，假定实例声明C（x）成立，算法从初始实例声明集A0＝｛C（x）｝开始；运用表1所示的算法规则，直到出现冲突或者没有规则可以再用。由扩展规则可以看出，如果术语描述C中不存在符号∪，则只是向A0中添加实例声明，不产生分支。如果术语描述C中存在符号∪，则会产生不确定的分支，只要任何一个分支是一致的，初始声明集A0就是一致的，即术语描述C是可满足的。检验流程图见图1。

图1 本体模型术语可满足性检验流程图

此算法规则只能在术语描述为否定范式的情况下才能使用，所以在使用规则前，应首先使用德摩根定律将术语描述C变换为否定范式。否定范式就是否定符号只能出现在概念术语前面的术语公式。使用以下转换我们可以将任何一个ALC术语描述转换为否定范式：

使用规则的过程中，如果有以下3种情况的任意一种出现，我们就可以认为产生冲突：

举例说明，给定模型的术语定义集和约束关系集分别如下：

对A⊆B进行验证，就是验证A∩﹁B是否是不可满足的，则术语描述C为：

下面给出术语描述C的可满足性判定过程：

说明：（2）、（3）、（4）来自于（1）使用∩规则；（5）、（6）来自于（3）使用∃规则；（7）来自于（4）使用∀规则；（8）、（9）来自于（7）使用∪规则。由判定过程可以看出，分支（1）、（2）、（3）、（4）、（5）、（6）、（7）、（9）存在Q（y）和﹁Q（y），此分支发生冲突；分支（1）、（2）、（3）、（4）、（5）、（6）、（7）、（8）不存在冲突，因此术语描述C是可满足的，即给定模型是不一致的。

4 Racer推理机

4.1 Racer简介

Racer（Renamed Abox and Concept Expression Reasoner）［2～4］是由 V.Haarslev和 R.MÖller编写的基于描述逻辑的推理机，是一种采用描述逻辑为理论基础的本体推理机。不仅可以当作描述逻辑系统使用，还可以用作语义知识库系统。Racer是基于描述逻辑Tableau算法，提供了对TBox和ABox的推理功能。利用Racer的查询推理机制可以对本体模型中的TBox和ABox的一致性进行推理，从而发现不一致信息。

Racer的主要查询推理功能如下［5～9，11］：

（1）基本的对于本体的满足性测试，本体的一致性通过满足性测试来实现。本体作为建模和语义描述的工具，如果产生不一致的情况，就会使得本体应用的领域产生形式和语义的矛盾，使得在本体上的具体工作产生歧义。

（2）对于包含性的测试也可转化为对满足性的测试。通过对包含性的测试，使得TBox中的概念划分了层次，形成了概念层次，便于计算概念描述的父（或者子）描述，以及计算其祖先和后代的概念描述。

（3）实例检测可以为某些个体确定相应的概念描述。并且可以对属于某些概念描述的个体进行分类。

（4）一些辅助的推理功能也是具体应用的重要工具。比如在知识库中对概念名字和个体名字的检索，与角色相关的个体对的检索，还有角色层次的检索，即角色的父子层次等。

4.2 实例验证

给出一个关于海军军械保障的本体模型的术语定义集、约束关系集和实例声明集分别如下：Tc＝｛AmmunitionSupport≡Ammunition∩Support，MineSupport≡Mine∩Support，MissileSupport≡Missile∩Support，TorpedoSupport≡Torpedo∩Support｝

其中，AmmunitionSupport≡Ammunition∩Support表示术语弹药保障可以用弹药和保障两个术语来表示，其余用法相同。Rc＝｛LogisticSupport⊆Support，OperationalSupport⊆Support，NavalOperationalSupport⊆OperationalSupport，NavalOrdnanceTechnicalSupport⊆ OperationalSupport，OrdnanceSupport⊆LogisticSupport，AmmunitionSupport≡OrdnanceSupport，MissileSupport⊆OrdnanceSupport，TorpedoSupport⊆Ordnance-Support，MineSupport⊆ OrdnanceSupport，OrdnanceSupport≡OrdnanceTechnicalSupport，AmmunitionSupport⊆AmmunitionTechnicalSupport，MineSupport≡ MineTechnicalSupport，Missile-Support≡MissileTechnicalSupport，TorpedoSupport≡TorpedoTechnicalSupport，LogisticSupport⊆﹁OperationalSupport，AmmunitionSupport⊆﹁MissileSupport，AmmunitionSupport⊆ ﹁ Mine-Support，AmmunitionSupport⊆ ﹁ TorpedoSupport，MissileSupport⊆ ﹁ MineSupport，Missile-Support⊆﹁TorpedoSupport，MineSupport⊆﹁TorpedoSupport｝

其中，LogisticSupport⊆Support表示后勤保障是保障的子类，OrdnanceSupport≡Ordnance-TechnicalSupport表示军械保障和军械技术保障是等价类，LogisticSupport⊆﹁OperationalSupport表示后勤保障和作战保障是互不相交的类，其余用法相同。Xd＝｛MineSupport（xxxMineTechnicalSupport），MissileSupport（xxxMissileTestE-quipmentMeasuringSupport）， TorpedoSupport（xxxTorpedoTechnicalSupport）｝

其中，MineSupport（xxxMineTechnicalSupport）表示xxx型水雷技术保障是水雷保障的一个实例，其余用法相同。

将以上的三个集转换为Racer的语法来表示，其中术语定义集Tc和约束关系集Rc对应于Tbox；实例声明集对应于Abox。代码如下：

用Racer对Tbox和Abox分别进行一致性检验，将会得到如下信息：

若在约束关系集中加入约束关系AmmunitionSupport⊆OperationalSupport，由约束关系集中原有的约束关系OrdnanceSupport⊆Logistic－Support、AmmunitionSupport⊆OrdnanceSupport和LogisticSupport⊆﹁OperationalSupport，可以推理得出 AmmunitionSupport⊆﹁Operational－Support，与新加入的约束关系发生语义冲突。因此，如果将（implies AmmunitionSupport OperationalSupport）加入到Racer推理机的Tbox代码中，将会得到如下概念冲突信息：

若在实例声明集中加入实例声明MissileSupport（xxxTorpedoTechnicalSupport），由约束关系MissileSupport⊆﹁TorpedoSupport和实例声明TorpedoSupport（xxxTorpedoTechnicalSupport）可以推断出xxxTorpedoTechnicalSupport不可能是MissileSupport的一个实例，实例声明集发生冲突。因此，如果将（instance xxxTorpedoTechnical-Support MissileSupport）加入到Abox中，将会得到如下实例冲突信息：