計算機科學家邏輯/謂詞邏輯/SATCHMO

SATCHMO

SATCHMO 定理證明器是最早使用模型生成的系統之一，即自下而上的證明過程。該證明器由一個小型的 Prolog 程式給出，該程式實現了一個表格證明過程。一個限制是，它需要範圍受限公式。

定義 30

一階子句 $A_{1}\lor \cdots \lor A_{n}\gets B_{1}\land \cdots \land B_{m}$ 稱為 *範圍受限*，如果出現在頭部 $A_{1}\lor \cdots \lor A_{n}$ 中的每個變數也出現在主體 $B_{1}\land \cdots \land B_{m}$ 中。

將子句轉換為範圍受限形式
$q(x)\lor p(x,y)\gets q(x)\qquad \rightsquigarrow \qquad q(X);p(X,Y)<-q(X),dom(Y)$
在 Prolog 資料庫中斷言範圍受限子句和 dom 子句。
呼叫 satisfiable

kill satisfiable :-    assume(X) :- asserta(X).     
       (Head <- Body)            assume(X) :-  
       Body, not Head, !,          retract(X), !, fail.  
       component(HLit, Head),      component(E, (E ; _)).      
       assume(HLit),               component(E, (_ ; R)) :-    
       not false,                   !, component(E, R).   
       satisfiable.                component(E, E).  
  satisfiable.

透過級別飽和修改實現一階完備性。該證明過程在地面情況下實現了超表格。

超表格 - 地面情況

所有開放分支僅包含正文字。以以下子句集為例 $\{\to A,\quad \to B,\quad A\land B\to C\lor D,\quad A\land B\to E\lor D,\quad A\land C\to \}$

定義 31（文字樹，子句表格）

一個 *文字樹* 是一個對 $(t,\lambda )$ ，由一個有限的、有序的樹 $t$ 和一個標記函式 $\lambda$ 組成，該函式將文字分配給 $t$ 的每個非根節點。

在一個有序樹 $t$ 中，節點 $N$ 的 後繼序列 是所有直接前驅為 $N$ 的節點的序列，按照 $t$ 給出的順序排列。

一組子句 ${\mathcal {S}}$ 的 （子句）真值表 $T$ 是一個文字樹 $(t,\lambda )$ ，其中，對於 $t$ 中的每個後繼序列 $N_{1},\dots ,N_{n}$ ，分別標記為文字 $K_{1},\dots ,K_{n}$ ，都存在一個替換 $\sigma$ 和一個子句 $\{L_{1},\dots ,L_{n}\}\in {\mathcal {S}}$ ，使得對於每個 $1\leq i\leq n$ 都有 $K_{i}=L_{i}\sigma$ 。 $\{K_{1},\dots ,K_{n}\}$ 稱為 真值表子句，真值表子句的元素稱為 真值表文字。

定義 32 (分支、開放和封閉真值表、選擇函式)

A branch of a tableau $T$ is a sequence $N_{0},\ldots ,N_{n}$ ( $n\geq 0$ ) of nodes in $T$ such that $N_{0}$ is the root of $T$ , $N_{i}$ is the immediate predecessor of $N_{i+1}$ for $0\leq i<n$ , and $N_{n}$ is a leaf of $T$ . We say branch $b=N_{0},\ldots ,N_{n}$ is a prefix of branch $c$ , written as $b\leq c$ or $c\geq b$ , iff $c=N_{0},\ldots ,N_{n},N_{n+1},\ldots ,N_{n+k}$ for some nodes $N_{n+1},\ldots ,N_{n+k}$ , $k\geq 0$ . The branch literals of branch $b=N_{0},\ldots ,N_{n}$ are the set $lit(b)=\{\lambda (N_{1}),\ldots \lambda (N_{n})\}$ . We find it convenient to use a branch in place where a literal set is required, and mean its branch literals. For instance, we will write expressions like $A\in b$ instead of $A\in lit(b)$ .

為了記住一個分支包含矛盾這一事實，我們允許將一個分支標記為開放或封閉。如果真值表中的每個分支都是封閉的，那麼該真值表是封閉的，否則它是開放的。

選擇函式是一個全函式 $f$ ，它將一個開放的 tableau 對映到它的一個開放分支。如果 $f(T)=b$ ，我們也說 $b$ 被選擇在 $T$ 中由 $f$ 。

請注意，分支始終是有限的，因為 tableau 是有限的。幸運的是，對使用哪種選擇函式沒有限制。例如，可以使用一個始終選擇“最左側”分支的選擇函式。

定義 33 (超 Tableau - 基本情況)

設 $S$ 是一個有限的子句集，而 $f$ 是一個選擇函式。對於 $S$ 的超 Tableau 如下所示遞迴定義
初始化步驟：一個單節點文字樹是 $S$ 的超 Tableau。它的單個分支標記為“開啟”。

超擴充套件步驟：如果

$T$ 是 $S$ 的一個開放超 Tableau， $f(T)=b$ （即 $b$ 被選擇在 $T$ 中由 $f$ ）具有開放的葉節點 $N$ ，並且
$C=A_{1},\ldots ,A_{m}\gets B_{1},\ldots ,B_{n}$ 是 $S$ 中的一個子句（ $m\geq 0$ ， $n\geq 0$ ），在此上下文中稱為擴充套件子句，並且
使得 $\{B_{1},\ldots ,B_{n}\}\subseteq b$ （稱為 *超條件*）。