歸結反演系統

歸結反演系統，以歸結原理為基礎、用歸謬法來證明數學定理的計算機軟體系統，機器定理證明的主要類型之一。在歸結反演系統中，定理證明是按以下幾步進行的：(1)否定目標公式，然後將這個否定式(?W)併到已知公式集S中去，形成一個擴充的公式集。這樣做的目的，是希望在後面幾步中能揭示這個擴充集存在矛盾，從而得出?W為假而W為真的結論，就是為了運用歸謬法。(2)將已擴充的公式集化成一個子句集。把公式化為子句有許多技巧，但歸根到底是利用根據真值表所建立起來的等價公式。(3)將歸結原理反覆套用於子句集，直到產生空子句為止。所謂歸結原理是說：兩個子句，若它們含有互補的正文字和反文字，則可以把互補的正反文字消除而將這兩個子句歸結為一個新的子句。一旦通過歸結得到空子句，即說明定理已經證出。