关系从句逻辑【Relational clausal logic】

命题从句逻辑是相当粗粒度的，因为它以命题【propositions】（即任何可以被赋予真值的事物）作为其基本构建块。例如，在命题逻辑中不可能形成以下论点：

Peter likes all his students
Maria is one of Peter’s students
Therefore, Peter likes Maria

为了使这种类型的推理形式化，我们需要讨论像 Peter 和 Maria 这样的个体，像 Peter 的学生这样的个体集合，以及个体之间的关系，比如 “喜欢”。命题分句逻辑的这种改进将我们引向关系分句逻辑。

Syntax

个体的名称称为常量【constants】；我们遵循 Prolog 约定，将它们写为以小写字符开头的单个单词（或用单引号括起来的任意字符串，例如 'this is a constant' ）。任意个体由变量【variables】表示，变量【variables】是以大写字符开头的单个单词。常量【constants】和变量【variables】共同表示为项【terms】。基本项【ground term】指的是没有变量【variables】的项【term】。

个体之间的关系由谓词【predicates】抽象表示(遵循与常量相同的符号约定)。原子【atom】是一个后面紧跟许多项【term】的谓词【predicates】，其中，这些项【term】用括号括起来，用逗号分隔，例如 likes(peter,maria)。括号之间的项【term】称为谓词【predicates】的参数【arguments】，参数【arguments】的数量就是谓词的【arity】。假定一个谓词【predicates】的【arity】是固定的，那么同名但不同的谓词被认为是不同的（类比为编程语言中的方法重载）。基本原子【 ground atom】是一个没有变量的原子。

与命题从句逻辑的语法有关的所有其余定义，特别是文字【literal】、从句【clause】和程序【program】的定义，都保持不变。因此，下面的从句【clauses】是用来表示上述语句的：

likes(peter,S):-student_of(S,peter). student_of(maria,peter).

这些从句的本意分别是：

“如果 S 是 Peter 的学生，那么 Peter 喜欢 S”
“Maria 是 Peter 的学生”
“Peter 喜欢 Maria”

很明显，我们希望可以在前两个从句的基础上，在逻辑上得出第三个从句，并且我们希望能够通过归结【resolution】来证明它。因此，我们必须扩展语义【semantics】和证明理论【proof theory】，以处理变量。

Logical variables

子句逻辑中的变量与数学公式中的变量非常相似:它们都是占位符，可以由来自赫布兰德宇宙【Herbrand universe】的任意基本项【ground term】替换。需要注意的是，逻辑变量在从句【clause】中是全局的（例如，如果变量出现在从句中的多个位置，它应该被相同的项【term】替换），但在程序中不是这样（即变量在程序内并不需要全局）。这可以从关系从句逻辑的语义中清楚地看出这一点，其中基本替换【grounding substitutions】应用于从句【clause】而不是程序。因此，根据定义，两个不同从句【clause】中的变量是不同的，即使它们有相同的名称。重命名子句中的变量有时会很有用，这样就不会有两个子句共享同一个变量；这被称为从句标准化【standardising the clauses apart】。

Semantics

程序 P 的赫布兰德宇宙【Herbrand universe】是出现在程序中的基本项（即常量）集【set of ground terms】。对于上述程序，赫布兰德宇宙【Herbrand universe】是 { peter, maria }。赫布兰德宇宙【Herbrand universe】是我们在从句中所讨论的所有个体【individuals】的集合。程序 P 的赫布兰德基【Herbrand base 】是一组基本原子集【set of ground atoms】，其中基本原子【ground atoms】是由程序 P 中的谓词和赫布兰德宇宙【Herbrand universe】中的基本项【ground terms】来构建组成。这个集合代表了我们能说的关于赫布兰德宇宙【Herbrand universe】中个体的所有事情。

上述程序的赫布兰德基【Herbrand base 】是：

{ likes(peter,peter), likes(peter,maria), likes(maria,peter), likes(maria,maria), student_of(peter,peter), student_of(peter,maria), student_of(maria,peter), student_of(maria,maria) }

如前所述，赫布兰德解释【Herbrand interpretation】是赫布兰德基【Herbrand base】的子集，其素被赋真值 true。例如：

{ likes(peter,maria), student_of(maria,peter) }

这就是上述程序的赫布兰德解释【Herbrand interpretation】。

显然，我们希望这种解释是程序的一个模型，但现在我们必须处理程序中的变量。替换是从变量【variables】到项【terms】的映射。例如， { S → maria } 和 { S → X } 就是替换。替换可以应用于从句【clause】，这意味着在替换中，出现在左边的所有变量【variables】都被替换为右边的项【terms】。例如，如果 C 是一个子句：

likes(peter,S):-student_of(S,peter).

然后上述的替换产生了下面的从句：

likes(peter,maria):-student_of(maria,peter). likes(peter,X):-student_of(X,peter).

注意第一个从句【clause】是一个基本从句【ground clause】；它被称为从句 C 的一个基本实例【ground instance】，并且替换 { S → maria } 被称为一个基本替换【grounding substitution】。基本从句【ground clause】中的所有原子【atom】都出现在赫布兰德基【Herbrand base】中，因此使用基本从句【ground clauses】进行推理就像使用命题从句【propositional clauses】进行推理一样。如果一个解释是该从句的每个基本实例【ground instance】的模型，则它是该非基本从句【non-ground clause】的模型。因此，为了证明

M = { likes(peter,maria), student_of(maria,peter) }

是上面从句 C 的一个模型，我们必须构造赫布兰德宇宙【Herbrand universe】 { peter, maria }上的基本实例集【set of the ground instances】，即：

{ likes(peter,maria):-student_of(maria,peter), likes(peter,peter):-student_of(peter,peter) }

并证明 M 是这个集合中每个素的模型。

Exercise 2.6

子句 C 在赫布兰德宇宙【Herbrand universe】 { peter, maria } 上有多少个模型？

likes(peter,S):-student_of(S,peter).

Answer 2.6

该从句的基本实例集【set of ground instances】是：

{ likes(peter,maria):-student_of(maria,peter), likes(peter,peter):-student_of(peter,peter) }

其赫布兰德基【Herbrand base】是：

{ likes(peter,peter), likes(peter,maria), likes(maria,peter), likes(maria,maria), student_of(peter,peter), student_of(peter,maria), student_of(maria,peter), student_of(maria,maria) }

只有四个基本原子【ground atom】与确定解释是否为模型有关。对这些基本原子【ground atom】的 $2 ^ {4} = 16$ 个真值赋值中，有 9 个会产生出一个模型。因为有 4 个不相关的基本原子【ground atom】，这就产生了 $9 * 2^{4} = 144$ 个模型。请注意，对于这样一个适度的赫布兰德宇宙【Herbrand universe】，这是一个相当大规模的模型，而且是这样一个简单的从句【clause】！这说明更少的知识会导致更多的模型。

{ likes(peter,peter),   likes(peter,maria), student_of(peter,peter), student_of(maria,peter)}


likes(peter,peter)	0	0	0	0	0	0	0	0	1	1	1	1	1	1	1	1
likes(peter,maria)	0	0	0	0	1	1	1	1	0	0	0	0	1	1	1	1
student_of(peter,peter)	0	0	1	1	0	0	1	1	0	0	1	1	0	0	1	1
student_of(maria,peter)	0	1	0	1	0	1	0	1	0	1	0	1	0	1	0	1
从句	1	0	0	0	1	1	0	0	1	0	1	0	1	1	1	1

Proof theory

因为使用基本从句【 ground clauses】进行推理就像使用命题从句进行推理一样，关系从句逻辑中的朴素证明方法将在应用归结【resolution】之前对程序中的每个从句应用基本替换【grounding substitutions】。这种方法是幼稚的，因为一个程序有许多不同的基本替换【grounding substitutions】，其中大多数不会导致归结证明。例如，如果赫布兰德宇宙【Herbrand universe】包含四个常量【constant】，则具有两个不同变量【variables】的从句【clause】就拥有 $2 ^ {4} = 16$ 个不同的基本替换【grounding substitutions】，而由三个此类从句组成的程序就拥有 16 * 16 * 16 = 4096 个不同的基本替换【grounding substitutions】。

在尝试应用归结【resolution】之前，我们不会应用任何基本替换【grounding substitutions】，而是由从句本身推导出所需的替换。会想一下，为了应用命题归结【propositional resolution】，被归结【resolved】的文字【literal】应该出现在两个输入从句【clause】中（在一个从句中是正文字，在另一个从句中是负文字）。在关系从句逻辑中，原子【atoms】可以包含变量【variables】。因此，我们不要求两个从句中出现完全相同的原子【atom】；相反，我们要求有一对原子可以通过替换（即用项替换变量【substituting terms for variables】）而使其相等。例如，假设程序 P 如下所示：

likes(peter,S):-student_of(S,peter). student_of(maria,T):-follows(maria,C),teaches(T,C).

第二个子句的意思是：“ Maria 是任何教授她所学课程的老师的学生”。从这两个从句我们应该能够证明“如果 Maria 学习 Peter 教授的课程，那么 Peter 喜欢 Maria”。这意味着我们通过 student_of 文字归结这两个从句。

student_of(S,peter) 和 student_of(maria,T) 这两个原子可以通过替换 { S → maria, T → peter } ，用 maria 替换 S ，用 peter 替换 T ，就可以变得相等。这个过程称为合一【unification】，而替换则称为合一子【unifier】。应用此替换会产生以下两个从句：

likes(peter,maria):-student_of(maria,peter). student_of(maria,peter):-follows(maria,C),teaches(peter,C).

请注意，第二个子句不是基本从句！！！

我们现在可以以通常的方式构造归结式【resolvent】，通过删除被归结的文字，并组合剩余的文字，从而产生所需的从句【clause】：

likes(peter,maria):-follows(maria,C),teaches(peter,C).

Exercise 2.7

写一个子句，表示 Peter 教授所有一年级的课程，并将归结【resolution】应用于该从句和上述的归结式【resolvent】。

Answer 2.7

下面是表示 Peter 教授所有一年级的课程的从句：

teaches(peter,C):-first_year_course(C).

然后将该从句与前面的归结式【resolvent】进行归结【resolution】，得到如下归结式【resolvent】：

likes(peter,maria):-follows(maria,C),first_year_course(C).

换句话说：“如果 Maria 上了一年级的课程，Peter 就会喜欢她。”

考虑下面的程序 P'

likes(peter,S):-student_of(S,peter). student_of(X,T):-follows(X,C),teaches(T,C).

它与前面的程序 P 的不同之处在于第二个从句中的常量 maria 已被一个变量【variable】替换。由于这将这一从句的适用性【applicability】从 maria 推广到 Peter 的任何学生，因此程序 P' 在赫布兰德宇宙【Herbrand universe】（包括 maria ）上的模型，也是程序 P 的模型，因此 P′⊨P。

特别的是，这意味着 P' 的所有逻辑结论【logical consequences】也是 P 的逻辑结论【logical consequences】。例如，我们可以从程序 P' 中通过合一子【unifier】 { S → maria, X → maria, T → peter } 推导【derive】出如下从句：

likes(peter,maria):-follows(maria,C),teaches(peter,C).

合一子【Unifiers】不一定需要是基本替换【grounding substitutions】： { X → S, T → peter } 这一替换【substitution】也合一【unifies】了两个 student_of 文字，然后这两个从句【clause】归结为：

likes(peter,S):-follows(S,C),teaches(peter,C).

第一个合一子【unifier】用项【term】替换了比严格必要的变量更多的变量（译注：简而言之，就是替换了一些本可以无需替换的变量，这些无需替换的变量并不影响归结），而第二个则只包含合一输入从句中的两个原子所必需的替换。因此，第一个归结式【resolvent】是第二个归结式【resolvent】的特殊情况，第二个归结式【resolvent】可以通过附加替换 { S → maria } 得到。因此，第二个归结式【resolvent】据说比第一个更通用。同样地，第二个合一子【unifier】被称为比第一个更通用的最广合一子/最一般合一子【most general unifier (mgu)】

可以说，最广归结式/最一般归结式【more general resolvents】概括了许多不那么一般的归结式【resolvent】。因此，在将归结【resolution】应用于带有变量的子句时，只导出【derive】那些尽可能一般的归结式【resolvent】是有意义的。这意味着我们只对两个文字的最广合一子/最一般合一子【most general unifier (mgu)】感兴趣。这样的 mgu，如果存在，除了任意重命名变量(例如，我们可以决定保留变量 X ，并用 X 替换 S )之外，总是唯一的【unique】。如果一个合一子【unifier】不存在，那么我们就说两个原子是不可合一【unifiable】的。例如，原子 student_of(maria,peter) 和原子 student_of(S,maria) 就是不可合一【unifiable】的。

正如我们之前看到的，从句逻辑中的实际证明方法是通过反证【proof by refutation】。如果我们成功地导出【deriving】了空子句【empty clause】，那么我们已经证明了在足以合一【unification】从句中的文字所需的替换【substitutions】下，子句集是不一致【inconsistent】的。例如，考虑程序：

likes(peter,S):-student_of(S,peter). student_of(S,T):-follows(S,C),teaches(T,C). teaches(peter,ai_techniques). follows(maria,ai_techniques).

如果我们想知道 Peter 是否有喜欢的人，我们在程序中添加对这个陈述【statement】的否定，即“Peter 不喜欢任何人”或 :-likes(peter,N)；该从句【clause】被称为一个查询【query】或一个目标【goal】。然后，我们尝试通过归结【resolution】找到不一致来反驳这个查询【query】。图 2.3 给出了一个反驳证明。在这个被称为证明树【proof tree】的图中，一行上的两个从句是归结【resolution】步骤的输入从句，它们通过直线连接到它们的归结式【resolvent】，然后它又是下一归结【resolution】步骤的输入从句，以及另一个程序从句。mgu 也在图中显示出来了。由于推导出了空子句【empty clause】，因此该查询【query】确实被反驳了，但仅在替换 { N → maria } 下，这构成了查询【quey】的答案。

通常，一个查询【query】可以有多个答案【answer】。例如，假设 Peter 不仅喜欢他的学生，还喜欢他的学生喜欢的人（以及那些人喜欢的人，以及……）：

likes(peter,S):-student_of(S,peter). likes(peter,Y):-likes(peter,X),likes(X,Y). likes(maria,paul). student_of(S,T):-follows(S,C),teaches(T,C). teaches(peter,ai_techniques). follows(maria,ai_techniques).

查询【query】 ?-likes(peter,N) 现在将有两个答案【answer】。

Exercise 2.8

画出答案 { N → paul } 的证明树。

Meta-theory

与命题归结【propositional resolution】一样，关系归结【relational resolution】也是健全的(即它总是产生输入子句的逻辑结论【logical consequence】)，驳斥完备【refutation complete】的(即它总是能检测到一组从句中的不一致)，但却不是完备的(即它并不总是产生输入子句的每个逻辑结论【logical consequence】)。关系从句逻辑的一个重要特征是，赫布兰德宇宙【Herbrand universe】(我们可以进行推理的个体集合)总是有限的。因此，这也意味着模型也是有限的，对于任何程序，不同模型的数量总是有限的。这意味着，原则上，我们可以通过列举 P 的所有模型，并检查它们是否也是 C 的模型，来回答这个问题“ C 是程序 P 的逻辑结论吗?”赫布兰德宇宙【Herbrand universe】的有限性将确保这个过程总是可以终止。这表明关系从句逻辑是可判定的【decidable】，因此（原则上）如果找不到更多答案，则可以防止解析归结。正如我们将在下一节中看到的，这不适用于全从句逻辑【full clausal logic】。

constant(peter). constant(maria). % rel_atom(A,L) <- A is a relational atom with arguments L rel_atom(likes(X,Y),[X,Y]). rel_atom(student_of(X,Y),[X,Y]). % Constants are the ground terms in relational clausal logic ground_term(T):- constant(T). ground_terms([]). ground_terms([T|Ts]):- ground_term(T), ground_terms(Ts). % An atom is ground if its arguments are ground terms ground_atom(A):- rel_atom(A,Args), ground_terms(Args).

今天的文章关系从句逻辑【Relational clausal logic】分享到此就结束了，感谢您的阅读。

关系从句逻辑【Relational clausal logic】

Syntax

Semantics

Proof theory

Meta-theory

相关推荐