利用目标公式作结束条件
在正向演绎系统中， 目标公式规定为文字的析取形式，当一个目标文字和与或图中的一个文字匹配式，可以将表示该目标文字的结点通过匹配弧连接到与或图中相应文字的结点上。表示目标文字的结点称为目标结点。当演绎系统产生的与或图包括一个在目标结点上结束的解图时，系统便成功的结束。
例如考虑下面问题：
事实表达式：A∨b
规则：A®c∧D和b®E∧G
目标公式：c∨G∨F
应用规则后得到的与或图如图3所示。
图1 与或图与目标文字的皮匹配
图中包含一个在目标结点上结束的解图，该结图对应的子句为c∨G。注意子句c∨G与目标公式不同，但比目标公式更一般。