通过一阶逻辑, 可定义一个子串(substr)的谓词, 该定义由以下的一组逻辑公式完成:
(1)
(2)
(3)
(4)
(5)
将这组一阶逻辑公式转化为子句标准形:
(1)
(2)
(3)
(4)
(5)
基于谓词substr的定义, 可以尝试求解这样的问题:
求满足
这里称
该目标的否命题是:
即:
接下来, 以子句标准形为基础进行归结。
(6)
(7)
(8)
(9)
(10)
(11)
于是, 得到一个替换
归结过程不是唯一的, 不同的归结过程可能带来不同的解。
事实上, 目标
一个霍恩子句(Horn Clause)具有以下的标准形式:
霍恩子句等价于
左边的
一个事实(Fact)是退化的霍恩子句:
一个数据库(Database)由若干个事实构成。
一个目标子句(Goal Clause)是另一种退化的霍恩子句:
在逻辑编程中, 一个程序子句(Program Clause)就是一个霍恩子句。
xxxxxxxxxx
101mother_child(trude, sally). /* m1 */
2
3father_child(tom, sally). /* f1 */
4father_child(tom, erica). /* f2 */
5father_child(mike, tom). /* f3 */
6
7sibling(X, Y) :- parent_child(Z, X), parent_child(Z, Y). /* s1 */
8
9parent_child(X, Y) :- father_child(X, Y). /* p1 */
10parent_child(X, Y) :- mother_child(X, Y). /* p2 */
运行:
xxxxxxxxxx
11?-sibling(sally, X).
其中,数据库包括事实m1和f1-f3; s1-s2和p1是程序子句。
目标等价于
对所有子句进行替换后, 继续进行下一步合一操作
等归结完成后,可得到替换
不过,除了"mei"之外,也会得到平凡解"ting".
xxxxxxxxxx
41?- sibling(ting, X).
2X = ting ;
3X = mei ;
4X = ting.
可通过修改sibling谓词的定义完善此程序。
xxxxxxxxxx
141mother_child(trude, sally).
2
3father_child(tom, sally).
4father_child(tom, erica).
5father_child(mike, tom).
6
7sibling(X, Y) :- parent_child(Z, X), parent_child(Z, Y), \+ X=Y.
8
9parent_child(X, Y) :- father_child(X, Y).
10parent_child(X, Y) :- mother_child(X, Y).
11
12?- sibling(ting, X).
13X = mei ;
14false.
在增加"\+ X=Y"后, 得到唯一解"mei".