[科普中国]-真值维护系统

基本数据结构

真值维护系统(TMS)有两种基本的数据结构：结点表示信念；理由(justification) 表示信念的原因。

TMS 的基本操作是：新结点的形成──将信念赋与该结点；一个结点的新理由的加入──表示把某个信念与该结点联接起来。在真值维护系统中，每一个命题或规则均称为结点，它分为两类：IN-结点，相信为真；OUT-结点，不相信为真，或无理由相信为真，或当前没有任何有效的理由。每个结点附有理由表，表中每一项表示具体结点的有效性。1

理由表在真值维护系统中有两类不同的理由表，一个称为支持表 SL(support list)，另一个称为条件证明 CP(conditional proof)。前者是它所在结点的信念之原因，即该信念的存在依赖于该表中的理由；而后者则是出现矛盾的原因，即一个矛盾结点的存在是该表中的理由所致。1

支持表SL({SL}() ())

这里，IN-结点表中的IN-结点表示知识库中的已知知识，而 OUT-结点表中的OUT-结点则表示这些结点的否定，不在知识库中，为默认知识。显然,如果 OUT-结点表为空，则该系统蜕化为单调推理。

(1) 现在是夏天 (SL ( ) ( ))

(2) 天气很潮湿 (SL (1) (3))

(3)天气很干燥

若结点(1)是 IN，结点(3)是 OUT，结点(2)才为 IN。这个证实表明：如果现在是夏天，又没有天气很干燥的证据；那么天气很潮湿。如果将来某一时刻出现了天气很干燥的证据，即为结点(3)提供了一个证据，则结点(2)就变为 OUT，因为它不再有一个有效的证实。像结点(2) 这样的结点称为假设，它与非空的 OUT 结点表的 SL证实有关。OUT 结点(3)是结点(2)之证实的一部分。但如果结点(3)不存在，就不能这样表示了。1

条件证明CP（{CP}（）（）（ ））

如果结论结点为IN-结点，以及下列条件成立：

（1）IN-假设中的每个结点都是IN-结点；

（2）OUT-假设中的每个结点都是OUT-结点。

那么条件证明CP是有效的。

一般说来，OUT-假设总是空集。TMS要求假设集划分成两个不相交的子集，分别为不导致的假设和导致矛盾的假设。

通常只要在IN-假设中的结点为IN，OUT-假设中的结点为OUT，则结论结点为IN。2

相关回溯步骤在知识库中出现不一致性时，寻找并删除已做的一个不正确的默认假设，恢复一致性。它包括下列三个步骤：

(1) 从产生的矛盾结点开始，回溯跟踪该矛盾结点的理由充足的支持以寻找矛盾的假设集，并从中去掉至少一个假设信念以消除矛盾。

(2) 构造一个结点记录矛盾产生的原因。这一步根据第一步收集到的“极大”假设集分 析导致矛盾的原因。

(3) 从S中选取假设Ai(即不合理假设)，并证实列在其理由充足的支持条件中的一个OUT-结点。1