| 正确性维持系统(Truth Maintenane System,TMS)是一个已经实现了的非单调推理系统。它用以协助其它推理程序维持系统的正确性，所以它的作用不是生成新的推理，而是在其它程序所产生的命题之间保持相容性。一旦发现某个不相容，它就调出自己的推理机制，面向从属关系的回溯，并通过修改最小的信念集来消除不相容。 |
| 在TMS中，每一命题或规则均称为节点，且对任一节点，以下两种状态必居其一： |
| IN相信为真 |
| OUT不相信为真，或无理由相信为真，或当前没有可相信的理由。 |
| 每个节点附有一证实表，表中每一项表示一种确定节点有效性的方法。IN节点是指那些至少有一个在当前说来是有效证实的节点。OUT结点则指那些当前无任何有效证实的节点。也许有人想知道为什么要不厌其烦地保留OUT结点?当然，花许多功夫去产生一些表示不正确命题的节点是没有意义的。但必须记住，在非单调推理系统中，产生一节点是以表示一个假定为真的命题，例如，使用缺省推理的结果。这时其余节点则在假设原始节点为IN的基础上产生。 |
| 但新信息的出现可能引起原始节点变成OUT(缺少信息时用缺省推理)，那时，一切基于它的节点都相应要变为OUT。不过，保留这些节点和它们的相互依赖性仍有用处。因为一旦有效信息发生了变化，而且引起原始节点再变为IN时，那些在它的基础上用来产生其它节点的推理就不必重作了。于是，当原始节点再变为IN时，其它各个节点的某个基于原始节点的证实将随之变为有效，这些节点也就变为IN了。 |
| 在系统中，有两种方式可用来证实一个节点的有效性可依赖于其它节点的有效性： |
| (1) 支持表(SL(IN 节点)(OUT 节点)) |
| (2) 条件证明(CP(结论) |
| (IN 假设) |
| (OUT 假设)) |
| 1.支持表(Support
List) 支持表最通用。如果在IN节点表中提到的节点当前都是IN，且在OUT节点表中提到的节点当前都是OUT，那么，它们是有效的。例如，下述节点： |
| (1)现在是冬天(SL( ) ( )) |
| (2)天气是寒冷的(SL(1) ( )) |
| 节点(1)的SL证实中的IN和OUT表为空，表明它不依赖于任何别的节点中当前的信念或缺少信念。这类节点称为前提。而节点(2)的SL证实的IN表中含节点(1)。这说明导致节点(2)可信任结论的推理链依赖于当前在节点(1)的信念。如果在将来某个时刻，TMS除掉了节点(2)的前提节点(1)，那么，由于节点(2)失去了依据，因而也要从IN表中除去。 |
| 综上所述，TMS的推理与直接的谓词逻辑系统相类似，除了它能撤消前提并对数据库的其余部分作适当的修改外，其余很相似。如果一个SL证实的OUT表不是空的，TMS也能处理缺省推理，如： |
| (1) 现在是冬天(SL( ) ( )) |
| (2) 天气是寒冷的(SL(1) (3)) |
| (3) 天气是温暖的 |
| 若节点(1)是IN，节点(3)是OUT，节点2才为IN。这个证实实际上是说：“如果现在是冬天，又没有天气是温暖的证据，则结论为：天气是寒冷的”。如果在将来某一时刻，出现了天气是温暖的证据(即为节点(3)提供了一个证实)，那么TMS将使节点(2)变为OUT，因为它不再有一个有效的证实。像节点(2)这样的节点(它们为IN是根据一个含有非空OUT表的SL证实)被称为假设。本例再次说明有必要存贮节点，甚至存贮那些为OUT的节点。节点(3)为OUT构成节点(2)之证实的一部分。但如果节点(3)不存在，就不能这样表示。值得注意的是，TMS本身并不产生证实。节点(2)的证实来自冬季一般天气是寒冷的这样一个领域的知识。由此，这个证实必须由使用TMS的问题求解程序提供。TMS能作的仅是利用证实来维持一个相容的信念数据库。 |
| 2.条件证明(Condition
Prove) 条件证明(CP)的证实表示有前提的论点。无论何时，只要在IN假设中的节点为IN，OUT假设中的节点为OUT，则结论节点往往为IN。于是，条件证明的证实有效。处理CP比SL更难。事实上，TMS是通过把它们转换成SL证实来进行处理的。 |
| TMS将显式证实与当前相信为真(即在IN表上)的命题一起存贮。当查出不相容时，它只消除必须删去者。如前所述，此过程称为面向从属关系的回溯。我们仍用安排会议的问题来说明它如何工作。设从节点(1)、(2)开始， |
| (1) 日期(会议)=星期三(SL( ) (2)) |
| (2) 日期(会议)≠星期三 |
| 目前没有相信“开会日期不应是星期三”的证实，所以节点1是IN以表示日期为星期三这一假设。 |
| 经某些推理后，安排会议系统得出会议必须在下午2∶00举行的结论，这是根据若干节点得出来的。这样一来，有如下节点： |
| (1) 日期(会议)=星期三(SL( )(2)) |
| (2) 日期(会议)≠星期三 |
| (3) 时刻(会议)=14∶00(SL(57，103，45) ( )) |
| 节点(1)、(3)在IN，节点(2)在OUT。现在，安排会议的程序要找一间房子，结果发现星期三下午两点钟无空房可供会议使用。于是通过产生下一节点来告诉TMS： |
| (4) 矛盾(SL(1，3) ( )) |
| 这时，调用面向从属关系的回溯过程。它查看矛盾节点的SL证实中的节点，比如说A1…Ak，然后向后跟踪，通过Ai的SL证实中的节点，比如说B1…Bs，再回到B的SL证实中的节点，继续寻找假设，试图找到这样一个假设集，只要除去该集中一个假设，矛盾就可消除。 |
| 在此例中，这个集只包含一个元素，即节点(1)，回溯机制通过产生一个不相容节点来记录它，不相容节点表示不相容的假设集。于是得到下面的节点集： |
| (1) 日期(会议)=星期三(SL( ) (2)) |
| (2) 日期(会议)≠星期三 |
| (3) 时间(会议)=14∶00(SL(57，103，45) ( )) |
| (4) 矛盾(SL(1，3) ( )) |
| (5) 不相容N-1(CP4(1，3) ( )) |
| 现在TMS选择不相容假设中的一个(这里只有节点(1)，所以选择是简单的事)，并且通过使节点(1)的OUT表中的一个节点变为IN来使节点(1)变为OUT。(因为一切假设都有非空的OUT表，所以可以这样作)。本例中又只有一个节点能使其为IN。使节点(2)为IN的方法就为节点(2)提供了一个以不相容节点为根据的证实。于是，我们现在有： |
| (1) 日期(会议)=星期三(SL( ) (2)) |
| (2) 日期(会议)≠星期三(SL(5) ( )) |
| (3) 时间(会议)=14∶00(SL(57，103，45) ( )) |
| (4) 矛盾(SL(1，3) ( )) |
| (5) 不相容N1(CP4(1，3) ( )) |
| 节点(2)与节点(5)为IN，就引起节点(1)为OUT，因为节点(1)的证实依赖于节点(2)是OUT。节点(4)现在也变成OUT。这样一来，矛盾就消除了，可选择一个新的日期。由于矛盾中不包含时间，所以仍保持下午2∶00不变。 |
|
|
 |