简介与/或形演绎推理方法

与/或形演绎推理又称基于规则的演绎推理。与前面讨论的归结演绎推理不同的是：不必再把有关知识转化为子句集，只需要把已知事实分别用蕴涵式及与/或形公式表示出来，再通过运用蕴涵式特性进行演绎推理以求证目标公式。按照其控制方向，基于规则的演绎推理又可分为正向、逆向和双向三种演绎形式。下面分别进行简单介绍。

（一）基于规则的正向演绎推理

1.与/或形变换及树形图表示

为了便于完成基于规则的正向演绎推理，首先将事实表示为谓词公式，并且设法通过与/或形变换，消去蕴涵符号，只在公式中保留否定、合取、析取符号，使该谓词表达式变换为标准的与/或形式公式。例如，蕴涵连接词用等值变换消去，使否定符号只作用到单个谓词，消去存在量词和全称量词等。

2.正向演绎推理的F规则及其标准化处理

所谓F规则，即正向演绎推理规则，表示为

式中，L为规则的前件，必须为单；W为规则的后件，可以是任意的与/或形公式。将任意公式变换为符合F规则定义的标准的蕴涵形式，称F规则标准化。其目的就是为了便于实施正向演绎推理。要对公式实施F规则标准，其一般步骤如下。

（1）暂时取消蕴涵符号。

（2）缩小否定符号辖域，把否定符“┐”运算直接移到具体文字前。

（3）可通过引入Skolem函数使变量标准化。

（4）化为前束式，并隐去全称量词。

（5）变换为标准F规则。

3.规则正向演绎推理过程

基于F规则的正向演绎推理过程为：

（1）必须把待证明的目标公式写成或转化为只有析取连接的公式；将事实公式变换为标准与/或形公式，画出事实与/或图；

（2）将所有正向推理规则变换为标准F规则；

（3）对与/或图的叶节点，搜索匹配的F规则，并把已经匹配的规则的后件添加到与/或图中；

（4）检查目标公式的所有文字是否全部出现在与/或图上，如果全部出现，则原命题（目标公式）得证。

注意　按照F规则进行事实匹配方法是：如果在系统规则库中找到某F规则L→W，并且其前件文字L恰好同与/或图中的某个叶节点的文字相同，则确定这条规则与该叶节点匹配。可把这条规则的前件加入事实与/或图，并在与其匹配的叶节点之间画双箭头作为匹配标记。同理，分解F规则的后件W，直到单个文字；将已经匹配的F规则的后件W，加入到与/或图中。

（二）基于规则的逆向演绎推理

所谓基于规则的逆向演绎推理，是从目标公式出发，逆向使用推理标准B规则的匹配，直到找出目标公式成立的已知事实依据条件时为止。(www.xing528.com)

因此，首先要将目标公式转换为标准与/或形公式，方法与规则正向演绎推理的事实表达式化为与/或形相同。

类似规则正向演绎推理中事实表达式的树形与/或图表示，这里也用树形与/或图来表示标准与/或形目标公式。与事实与/或图不同的是，这里规定用连接弧线标记目标公式与/或图中合取节点关系。

逆向演绎推理使用的标准B规则，表示为

式中，规则的前件W可为任意的与/或形公式；而规则的后件L，必须为单文字或单文字的合当规则后件L为多个单文字合取时，比如W→（L1∧L2∧…∧Lk），可以转换为K个单文字后件的B规则，即W→L1，W→L2，…，W→Lk。

B规则标准化过程和F规则标准化过程类似，即：

①暂时消去蕴涵符号；

②缩小否定符号辖域；

③引入Skolem函数，使变量标准化；

④前束化并隐去全称量词；

⑤恢复蕴涵而变换为标准B规则等。

寻找B规则匹配的过程中，注意寻找每个单文字后件与相应叶节点的匹配，若找到了匹配，则需要用匹配线标记匹配；匹配过程中有时需要进行置换、合一，要标出相应的置换关系；注意按前述相同方法拆分B规则的前件表达式，直到是单文字等。

总之，规则逆向演绎推理基本过程为：

（1）将目标公式化为标准与/或形式，画出相应的目标与/或图；

（2）将所有逆向推理规则变换为标准的B规则；

（3）按先事实、再规则的顺序，对于目标与/或图，若找到了事实匹配，做相应标记：若找到B规则匹配，则把此B规则添加到目标与/或图中，做相应的匹配标记；

（4）检查目标与/或图，如果所有叶节点都匹配到事实文字，则目标公式得到证明。至此，规则逆向演绎推理证明过程结束。

（三）规则双向演绎推理

如果一个系统给出了事实表达式，同时所给出的规则既有F规则，又有B规则，并给出了系统要证明的目标公式，这时仅仅单纯使用F规则的正向演绎推理，或仅使用B规则的逆向演绎推理，都将在证明中遇到难以克服的困难，因此该系统应该采用基于规则的双向演绎推理来解决。

所谓双向演绎推理，即在从基于事实的F规则正向推理出发的同时，从基于目标的B规则逆向推理出发，同时进行双向演绎推理。

双向演绎推理终止的条件：必须使得正向推理和逆向推理互相完全匹配。即所有得到的正向推理与/或图的叶节点，正好与逆向推理得到的与/或图的叶节点一一对应匹配。