規則演繹系統

規則演繹系統(rule-based deduction system )亦稱基於規則的演繹系統.它是一種求解問題、證明定理的計算機系統，而且是一種採用直接證明法思想(相對於歸結反演方式的反證法思想而言)的計算機系統。

此種系統又細分為規則正向演繹系統、規則逆向演繹系統以及規則雙向演繹系統三種.在規則演繹系統中，總將被求解的問題描述為:事實、規則和目標.規則正向演繹系統從事實出發，通過使用規則，試圖推導出所需目標.規則逆向演繹系統則從目標出發，通過使用規則，試圖推證出所需事實都存在.規則雙向演繹系統則結合使用正向與逆向兩種系統求解技術來求解問題、證明定理.規則演繹系統對被求解問題中的事實、規則和目標都有一定的限制，也即都有其使用條件.

1.規則正向演繹系統的使用條件:

1)事實表達式為任意謂詞公式.

2)規則形式為L->W(其中L為單文字，W為任意謂詞公式).

3)目標公式為文字析取式.

2.規則逆向演繹系統的使用條件:

1)事實表達式為文字合取式.

2)規則形式為W->L(其中L為單文字，W為任意謂詞公式).

3)目標公式為任意謂詞公式.