计算机科学家逻辑/谓词逻辑/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$ （称为 *超条件*）。