点击看大图
3 与/或形双向演绎推理
与/或正向演绎推理要求目标公式是文字的析取式
与/或逆向演绎推理要求事实公式是文字的合取式
与/或双向演绎推理由表示目标及表示已知事实的两个与/或树结构构成，这些与/或树分别由正向演绎的F规则及逆向演绎的B规则进行操作,F规则为单文字的左部，B规则为单文字的右部。
双向演绎推理的难点在于中止条件，只有当它们对应的叶结点都可合一时，推理才能结束。
 点击看大图