逻辑编程原理

通过一阶逻辑, 可定义一个子串(substr)的谓词, 该定义由以下的一组逻辑公式完成:

(1)$\mathrm{\forall }xsubstr(x,x)$$\forall x \, substr(x,x)$

(2)$\mathrm{\forall }x\mathrm{\forall }ysuffix(x,y\cdot x)$$\forall x \forall y\, suffix(x,y\cdot x)$

(3)$\mathrm{\forall }x\mathrm{\forall }yprefix(x,x\cdot y)$$\forall x \forall y \, prefix(x,x\cdot y)$

(4)$\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(substr(x,y)\wedge suffix(y,z)\to substr(x,z))$$\forall x \forall y \forall z \, \left( substr(x,y)\land suffix(y,z) \rightarrow substr(x,z) \right)$

(5)$\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }z(substr(x,y)\wedge prefix(y,z)\to substr(x,z))$$\forall x \forall y \forall z \, \left( substr(x,y)\land prefix(y,z) \rightarrow substr(x,z) \right)$

将这组一阶逻辑公式转化为子句标准形:

(1)$substr(x,x)$$substr(x,x)$

(2)$suffix(x,y\cdot x)$$suffix(x,y\cdot x)$

(3)$prefix(x,x\cdot y)$$prefix(x,x\cdot y)$

(4)$substr(x,y)\wedge suffix(y,z)\to substr(x,z)$$substr(x,y)\land suffix(y,z) \rightarrow substr(x,z)$

(5)$substr(x,y)\wedge prefix(y,z)\to substr(x,z)$$substr(x,y)\land prefix(y,z) \rightarrow substr(x,z)$

基于谓词substr的定义, 可以尝试求解这样的问题: 求满足$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$的$x$$x$.

这里称$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$为目标(Goal). 求解该问题的思路是: 结合替换, 通过归结方法证否该目标的否命题。然后, 问题的解可通过相应的替换得到。

该目标的否命题是: $\mathrm{\neg }(\mathrm{\exists }Xsubstr(w,a\cdot a\cdot a\cdot b\cdot c\cdot c))$$\lnot \left( \exists X\,substr(w,a\cdot a\cdot a\cdot b\cdot c\cdot c) \right)$

即: $\mathrm{\forall }X\mathrm{\neg }substr(w,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$\forall X\,\lnot substr(w,a\cdot a\cdot a\cdot b\cdot c\cdot c)$

接下来, 以子句标准形为基础进行归结。

(6)$\mathrm{\neg }substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$\lnot substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$

(7)$\mathrm{\neg }substr(X,y_1)\vee \mathrm{\neg }suffix(y_1,a\cdot a\cdot b\cdot c\cdot c)$$\lnot substr(X,\;y_1 ) \lor\ \lnot suffix(y_1,a\cdot a\cdot b\cdot c\cdot c)$

$6,4,\{x\leftarrow X,y\leftarrow y_1,z\leftarrow a\cdot a\cdot b\cdot c\cdot c\}$$6,4,\left\{ x \leftarrow X,\; y \leftarrow y_1,\; z \leftarrow a\cdot a\cdot b\cdot c\cdot c \right\}$

(8)$\mathrm{\neg }substr(X,a\cdot b\cdot c\cdot c)$$\lnot substr(X,\; a\cdot b\cdot c\cdot c)$

$7,2,\{x\leftarrow a\cdot b\cdot c\cdot c,y\leftarrow a,y_1\leftarrow a\cdot b\cdot c\cdot c\}$$7,2,\left\{ x \leftarrow a\cdot b\cdot c\cdot c,\; y \leftarrow a,\; y_1 \leftarrow a\cdot b\cdot c\cdot c \right\}$

(9)$\mathrm{\neg }substr(X,y_2)\vee \mathrm{\neg }suffix(y_2,a\cdot b\cdot c\cdot c)$$\lnot substr(X,\;y_2 ) \lor\ \lnot suffix(y_2, a\cdot b\cdot c\cdot c)$

$8,5,\{x\leftarrow X,y\leftarrow y_2,z\leftarrow a\cdot b\cdot c\cdot c\}$$8,5,\left\{ x \leftarrow X,\; y \leftarrow y_2,\; z \leftarrow a\cdot b\cdot c\cdot c \right\}$

(10)$\mathrm{\neg }substr(X,a\cdot b\cdot c)$$\lnot substr(X,\; a\cdot b\cdot c)$

$9,3,\{x\leftarrow a\cdot b\cdot c,y\leftarrow c,y_2\leftarrow a\cdot b\cdot c\}$$9,3,\left\{ x \leftarrow a\cdot b\cdot c,\; y \leftarrow c,\; y_2 \leftarrow a\cdot b\cdot c \right\}$

(11)$◻$$\Box$

$10,1,\{x\leftarrow X,\boxed{{\displaystyle X\leftarrow a\cdot b\cdot c}}\}$$10,1,\left\{ x \leftarrow X,\; \boxed{X \leftarrow a\cdot b\cdot c} \right\}$

于是, 得到一个替换$\{X\leftarrow a\cdot b\cdot c\}$$\{X \leftarrow a\cdot b\cdot c\}$, 正是这个替换使得目标的否不成立。也就是说替换$\{X\leftarrow a\cdot b\cdot c\}$$\{X \leftarrow a\cdot b\cdot c\}$是满足目标$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$的一个解。

归结过程不是唯一的, 不同的归结过程可能带来不同的解。 事实上, 目标$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$$substr(X,a\cdot a\cdot a\cdot b\cdot c\cdot c)$也确实存在不同的解。

一个霍恩子句(Horn Clause)具有以下的标准形式:

$A\leftarrow B_1,B_2,\cdots ,B_n$$A \leftarrow B_1,\,B_2,\,\cdots,\,B_n$

霍恩子句等价于$A\vee \mathrm{\neg }{B}_1\vee \mathrm{\neg }{B}_2\vee \mathrm{\neg }\cdots \vee \mathrm{\neg }{B}_n$$A{\lor\lnot} B_1{\lor\lnot}B_2{\lor\lnot}\cdots{\lor\lnot}B_n$.

左边的$A$$A$是头部(Head), 右边$\mathrm{\neg }{B}_i$${\lnot}B_i$称为身子(Body).

一个事实(Fact)是退化的霍恩子句: $A\leftarrow .$$A \leftarrow.$

一个数据库(Database)由若干个事实构成。

一个目标子句(Goal Clause)是另一种退化的霍恩子句: $\leftarrow B_1,B_2,\cdots ,B_n.$$\leftarrow B_1,\,B_2,\,\cdots,\,B_n.$

在逻辑编程中, 一个程序子句(Program Clause)就是一个霍恩子句。

xxxxxxxxxx
10
1
mother_child(trude, sally). /* m1 */
2

3
father_child(tom, sally). /* f1 */
4
father_child(tom, erica). /* f2 */
5
father_child(mike, tom). /* f3 */
6
 
7
sibling(X, Y) :- parent_child(Z, X), parent_child(Z, Y). /* s1 */
8
 
9
parent_child(X, Y) :- father_child(X, Y). /* p1 */
10
parent_child(X, Y) :- mother_child(X, Y). /* p2 */

运行:

xxxxxxxxxx
1
1
?-sibling(sally, X).

其中,数据库包括事实m1和f1-f3; s1-s2和p1是程序子句。

目标等价于$\mathrm{\neg }sibling(sally,X)$${\lnot}sibling(sally, X)$, 而子句s1等价于$sibling(X,Y)\vee \mathrm{\neg }parent\mathrm{\_}child(Z,X)\vee \mathrm{\neg }parent\mathrm{\_}child(Z,Y)$$sibling(X, Y){\vee\lnot}parent\_child(Z, X){\vee\lnot}parent\_child(Z, Y)$. 所以目标将与s1进行合一操作, 得到替换 $\{sally\leftarrow X,X\leftarrow Y\}$$\{sally{\leftarrow}X, X{\leftarrow}Y\}$

对所有子句进行替换后, 继续进行下一步合一操作

$\cdots \cdots$$\cdots\cdots$

等归结完成后,可得到替换$\{X\leftarrow mei\}$$\{X{\leftarrow}mei\}$为所求的解。

不过,除了"mei"之外,也会得到平凡解"ting".

xxxxxxxxxx
4
1
?- sibling(ting, X).
2
X = ting ;
3
X = mei ;
4
X = ting.

可通过修改sibling谓词的定义完善此程序。

xxxxxxxxxx
14
1
mother_child(trude, sally).
2
 
3
father_child(tom, sally).
4
father_child(tom, erica).
5
father_child(mike, tom).
6
 
7
sibling(X, Y) :- parent_child(Z, X), parent_child(Z, Y), \+ X=Y.
8
 
9
parent_child(X, Y) :- father_child(X, Y).
10
parent_child(X, Y) :- mother_child(X, Y).
11

12
?- sibling(ting, X).
13
X = mei ;
14
false.

在增加"\+ X=Y"后, 得到唯一解"mei".