子句逻辑与归结:理论背景

admin管理员组

文章数量:1531792

2.1 命题子句逻辑【Propositional clausal logic】

非正式地讲，命题【proposition 】是指任何要么对要么错的陈述【statement】，比如"2 + 2 = 4"或者"月亮是绿色奶酪做的"。这些是命题逻辑的基石，是最弱的逻辑形式。

语法【Syntax】

命题【Propositions 】由原子【atoms】抽象表示，原子是以小写字母开头的单个单词。 例如，married 就是一个原子【atom】，表示这样一个命题：“他/她已婚”； 同样，man 表示这样一个命题：“他是一个男人”。 使用特殊符号‘:-’ (if), ‘;’ (or) 和 ‘,’ (and)，我们可以将原子【atom】组合成子句【clauses】。 例如，

married;bachelor:-man,adult

这就是一个子句【clause】，它表达这样一个意思：“如果某人是个男人，并且是一个成年人，那么他要么已结婚，要么就还是单身汉【somebody is married or a bachelor if he is a man and an adult】”。if 符号':- '左边的部分称为子句的头【head】，右边的部分称为子句的体【body】。子句的头【head】总是原子【atom】的析取【disjunction】(or)，子句的体【body】总是原子【atom】的合取【conjunction】(and)。

--------------------------------------------------------------------------------------------------------------------------------

Exercise 2.1.1 

用"person"、“sad”、“happy”三个原子【atom】，把下列语句翻译成子句【clauses】:

1. persons are happy or sad;

2. no person is both happy and sad;

3. sad persons are not happy;

4. non-happy persons are sad.

Answer 2.1.1

这些语句应该以“if…then…”形式解读。

第一个语句读作"if somebody is a person, then she is happy or sad"

happy;sad:-person

第二个语句读作"if somebody is a person, then she is not both happy and sad"，在子句逻辑中，只能得出肯定结论 【positive conclusions】 ；否定结论【negative conclusions】 需要转化为肯定结论 【positive conclusions】，如下:“if somebody is a person, and she is happy and sad, then contradiction（矛盾）”，这里用一个空的子句头【head】来表明这是一个矛盾的结论（仔细看，:- 之前是空的）：

:-person,happy,sad

按照同样的方法，第三个语句可以读作“if somebody is a person who is sad, and she is happy, then contradiction”

:-person,sad,happy

因此，句子 2 和子句 3 传达了相同的逻辑意义。

最后，第四个语句读作“if somebody is a person who is not happy, then she is sad”。 在从句逻辑中，只能使用肯定条件【positive conditions】； 因此，这种否定条件【negative condition】需要转化为一个肯定条件【positive conditions】，即：“if somebody is a person, then she is sad or happy”。 因此，我们得到了与语句 1 相同的子句：

sad;happy:-person

--------------------------------------------------------------------------------------------------------------------------------

程序【program】是一个子句集【 set of clauses】，每个子句都以一个句点【.】结束。这些子句应合起来读；例如：

woman;man:-human.
human:-woman.
human:-man.

该程序意欲表达的意思是：

(if someone is human then she/he is a woman or a man)  and

(if someone is a woman then she is human)  and 

(if someone is a man then he is human)

或者，换句话说（一言以蔽之），“someone is human if and only if she/he is a woman or a man”。

语义【Semantics】

程序 P 的赫布兰德基【Herbrand base】是出现在程序  P 中的原子集【set of atoms】。对于上述程序，其赫布兰德基【Herbrand base】是  { woman, man, human }.。 赫布兰德解释【Herbrand interpretation】（或简称解释）是从赫布兰德基【Herbrand base】到真值集合  { true, false } 的映射。例如，映射  { woman → true, man → false, human → true }  是对上述程序的赫布兰德解释【Herbrand interpretation】。赫布兰德解释【Herbrand interpretation】可以被视为描述论域【Universe of Discourse】中可能的事态（在这种情况下:“she is a woman, she is not a man, she is human”）。 因为在我们考虑所的语义中只有两种可能的真值（即 true 和 false），因此我们可以通过仅列出被分配了真值 true 的原子【atom】，以此来简化这种映射；而根据定义，其余的原子【atom】被分配的真值即为 false。在这一约定下，赫布兰德解释【Herbrand interpretation】只不过是赫布兰德基【Herbrand base】的一个子集。因此，先前的赫布兰德解释【Herbrand interpretation】可以表示为 { woman, human }。

由于赫布兰德解释【Herbrand interpretation】给子句中的每个原子【atom】分配了真值，它也为整个子句分配了一个真值。根据子句【clause】中原子【atom】的真值确定该子句【clause】的真值的规则并不复杂，如果你记住：子句体【clause body】是原子【atom】的合取【conjunction】，而子句头【clause head】是原子的析取【disjunction】。因此，如果子句体【clause body】中的每个原子【atom】都为 true，则子句体【clause body】为 true；如果子句头【clause  head】中至少有一个原子【atom】为 true，则子句头【clause  head】为 true。反过来，子句的真值又由子句头【clause head】和子句体【clause body】的真值决定。有四种可能：

1. the body is true, and the head is true;

2. the body is true, and the head is false;

3. the body is false, and the head is true;

4. the body is false, and the head is false.

子句【clause】意欲表达的意思是“if body then head’”，在第一种情况下显然是 true ，在第二种情况下显然是 false。

剩下的两种情况呢？他们涵盖了如“if the moon is made of green cheese then 2 + 2 = 4”这样的陈述【statement】，其中子句头【clause head】与子句体【clause body】之间没有任何关系。有人会说，这样的陈述【statenmet】，既不是 true 也不是 false。然而，我们的语义还不够成熟，无法处理这样的问题：它所坚持的是，在每种可能的解释中，都应该为该子句分配一个真值。因此，只要其子句体【clause body】为 false，我们就认为该子句为 true 。 不难看出，在上述这 4 种真值条件【truth conditions】下，一个从句【clasuse】与 “head or not body” 这一陈述【statement】是等价的。 例如，子句 married;bachelor:-man,adult 可以被解读为“someone is married or a bachelor or not a man or not an adult”。因此，子句是关于原子的析取【disjunction】，如果原子【atom】出现在子句体【clasuse body】中，则它们被取反【negated】。因此，子句体【clasuse body】中的原子【atom】通常被称为负文字【negative literals】，而子句头中的原子被称为正文字【positive literals】。

总而言之：当且仅当以下条件中的至少一个为真时，一个子句【clause】才在解释中被分配真值 true ：

1. 子句体【clause body】中至少一个原子【atom】在解释【interpretation】中被分配的真值为 false （case 3/4）
2. 子句头【clause head】中至少一个原子【atom】在解释【interpretation】中被分配的真值为 true （case 1/3）

如果一个子句【clause】在一个解释【interpretation】中的真值为 true ，那么我们可以说该解释【interpretation】是该子句【clause】的模型【model】。例如，上面的程序有以下模型【model】: 

• ∅ (the empty model, assigning false to every atom),
• { woman, human }
• { man, human }
• { woman, man, human }

由于含有三个原子【atom】的赫布兰德基【Herbrand base】有八种可能的解释，这意味着该程序包含的信息足以排除其中一半。

向程序添加更多子句【clause】意味着限制其模型集【set of models】。 例如，如果我们在程序中添加子句 woman （一个没有子句体的子句），我们就可以排除第一个和第三个模型，只留下 { woman, human } 和 { woman, man, human } 这两个模型。 请注意，在这两个模型中，human 都是 true。 我们说 human 是该子句集【set of clauses】的一个逻辑结果【logical consequence，也称为蕴含】。一般来说，如果程序 P 的每个模型都是子句 C 的模型，那么该子句 C 就是该程序 P 的逻辑结论【logical consequence 】；我们写作 P⊨C。

--------------------------------------------------------------------------------------------------------------------------------

Exercise 2.1.2

给定如下程序：

married;bachelor:-man,adult.
man.
:-bachelor.

确定下列哪个子句是这个程序的逻辑结论【 logical consequences 】：

1. married:-adult;

2. married:-bachelor;

3. bachelor:-man;

4. bachelor:-bachelor.

Answer 2.1.2

首先来看程序中第一个子句，该子句的模型有很多，但是在程序的第二个子句中，man 必须为 true ，结合这两个子句，即第一个子句的模型 & man = true ，其对应的模型与子句 married;bachelor:-adult. 的模型一致。同样地，在程序的第三个子句中 bachelor 必须为 false ，如果我们再附加上 bachelor = false ，则对应的模型与子句 married:-married 的模型一致，那么 married:-adult; 即是该程序的逻辑结论【 logical consequences 】。

对于第二个子句 married:-bachelor ，它的子句体在程序中约束为必须为 false ，因此程序的任意模型对于子句 married:-bachelor 肯定为 true，因此它是该程序的逻辑结论【 logical consequences 】。

对于第三个子句 bachelor:-man ，它的子句体在程序中约束为必须为 true，而子句头又在程序中约束为必须为 false ，因此程序的任意模型对于子句 bachelor:-man 肯定为 false，因此它并不是该程序的逻辑结论【 logical consequences 】。

最后一个子句是一个重言式【tautology】，它在任何解释中都为 true，因此它是该程序的逻辑结论【 logical consequences 】

--------------------------------------------------------------------------------------------------------------------------------

在剩下的这两个模型中，显然 { woman, human } 是我们预期的模型；但是这个程序还没有包含足够的信息来将它与非预期模型  { woman, man, human } 区分开来。为此我们可以添加另一个子句【clause】，以确保原子 man 被映射为 false。例如，我们可以加上：

:-man

(it is not a man) 或者

:-man,woman

(nobody is both a man and a woman)

但是，将预期模型中为 false 通过这种方式显式的指出，这并不总是可行的。例如，考虑一个旅行社咨询航空公司数据库的情景：我们只是想说，如果某一航班（航班是由飞机、出发地、目的地、日期和时间的组合）未在数据库中列出，那么它就不存在，我们绝不会在数据库中列出列出某架飞机不是由阿姆斯特丹飞往伦敦的所有日期。

因此，与其一直添加子句，直到只剩下一个模型，我们更希望在语义中添加一条规则，该规则告诉我们在这几种模型【model】中哪一个是预期模型。航空公司的栗子告诉我们，通常情况下，我们只会在被迫的情况下，才愿意接受某事为 true ，也就是说，它在所有可能的模型中都为 true 。这意味着我们应该取程序的每个模型的交集，以构建预期的模型。在这个例子中，该交集是  { woman, human } 。注意，这个模型是最小的【minimal】，因为它的子集都不是模型。因此，这种语义被称为最小模型语义【minimal model semantics】。

注意：将模型与逻辑结论区分开～～

不幸的是，这种方法只适用于受限的一类程序。考虑以下程序：

woman;man:-human.
human.

这个程序有三个模型：

• { woman, human }
• { man, human }
• { woman, man, human }

这些模型的交集是  { human }，但是这个解释【interpretation】却并不是第一个子句的模型！该程序实际上有两个最小模型，而不是一个，这是由于程序中的第一个子句有一个析取头【disjunctive head】导致的。这样的子句也被称为不定子句【indefinite clause】，因为它不必允许得出明确的结论【it does not permit definite conclusions to be drawn】。

另一方面，如果我们只允许确定子句【definite clause】，即具有单个正文字【positive literal】的子句，则可以保证最小模型是唯一的。 我们将在 2.4 节处理确定子句【definite clause】，因为 Prolog 是基于确定子句逻辑【definite clause logic】的。 原则上讲，这意味着像 women;man:-human 这样的子句【clasuse】在 Prolog 中是不可表达的。 但是，这样的子句可以通过将子句头【clause head】中的一个文字移到子句体【clause body】中，并拓展一个额外的否定/取反操作，这样就可以将其转变为一个伪定子句【pseudo-definite clause】。但这带来了如下两种可能：

woman:-human,not(man).
man:-human,not(woman).

在 Prolog 中，我们必须在这两个子句之间进行选择，这意味着我们只有一个原始不定子句【indefinite clause】的近似值。 Prolog 中的否定/取反【Negation】是一个涉及很多方面的重要主题。 在第 3 章中，我们将展示 Prolog 如何处理子句体【clause body】中的否定/取反【negation】。 在第 8 章中，我们将讨论这种否定/取反【negation】的具体应用。

证明论【Proof theory】

回想一下，如果程序 P 的每一个模型都是子句 C 的模型，那么子句 C 就是程序 P 的逻辑结论【logical consequence】（ P⊨C)）。一般来说，校验这个条件通常是不可行/不现实的（译者注：穷举所有模型的话，这计算量很大，尤其当模型基数大的时候）。因此，我们需要通过推理规则【inference rules】，以一种更有效的方法来计算逻辑结论【logical consequence】。如果通过对这种推理规则【inference rules】的多次应用，我们可以从程序 P 推导出 C，我们就可以说 C 可以从 P 中证得。这种推理规则纯粹是语法的【syntactic】，并不涉及任何潜在的语义【semantics】。

子句逻辑【clausal logic】的证明理论由一个称为归结【resolution】的推理规则【inference rule】组成。归结【resolution】是一个非常强大的推理规则【inference rule】。考虑以下程序：

married;bachelor:-man,adult.
has_wife:-man,married.

这个简单的程序有不少于 26 个模型【model】，如果我们想校验一个子句是否是它的逻辑结论【 logical consequence 】，就需要考虑每个模型。

--------------------------------------------------------------------------------------------------------------------------------

Exercise 2.1.3

写下不是该程序的 6 种赫布兰德解释【Herbrand interpretation】。

Answer 2.1.3

这6个解释分别是

1. {man,adult}
2. {man,adult,has_wife}
3. {man,married}
4. {man,married,adult}
5. {man,married,bachelor}
6. {man,married,adult,bachelor}

前两种赫布兰德解释【Herbrand interpretation】满足【satisfy】了程序中第一个子句的子句体，但违背【violate】了它的子句头；

后四种赫布兰德解释【Herbrand interpretation】满足【satisfy】了程序中第二个子句的子句体，但违背【violate】了它的子句头。

--------------------------------------------------------------------------------------------------------------------------------

下面的子句是这个程序的逻辑结论【 logical consequence】：

has_wife;bachelor:-man,adult

通过归结【resolution】，只需要简单的一步即可得出该结论。 这一步代表了以下的推理过程：

• if someone is a man and an adult, then he is a bachelor or married;
• but if he is married, he has a wife;
• therefore, if someone is a man and an adult, then he is a bachelor or he has a wife

在这个论证中，程序中的两个子句通过原子【atom】 married 相互关联，它出现在第一个子句的子句头（一个正文字【positive literal】）和第二个子句的子句体（一个负文字【negative literal】）中。 派生子句【derived clause】也被称为归结式【resolvent】，它由两个输入子句中的所有文字组成，除了 married（被归结的文字）。 在两个输入子句中都出现的负文字 man ，在派生子句中只出现一次。 这个过程如图 2.1.1 所示。

注意：归结规则指的是由两子句通过归结得到归结式的规则，出自《计算机科学技术名词 》 (第三版)

Figure 2.1.1 A resolution step

当归结【resolution】被应用于确定子句【definite clauses】时，这是很容易理解的：

square:-rectangle,equal_sides.
rectangle:-parallelogram,right_angles.

应用归结【resolution 】产生如下子句：

square:-parallelogram,right_angles,equal_sides

也就是说，第一个子句的子句体中的原子【atom】 rectangle  ，被第二个子句（该子句以 rectangle 为子句头）的子句体所替换。这个过程也称为将第二个子句展开【unfolding 】到第一个子句中，如图 2.1.2 所示：

Figure 2.1.2 Resolution with definite clauses

由一个归结【resolution】步骤产生的归结式【resolvent】可以用作下一个步骤的输入。从程序 P 到子句 C 的证明【proof】或推导【derivation 】，其实是一个子句序列【sequence of clauses】，其中的子句要么来自程序中，要么是前面两个子句的归结式【resolvent】，而最后一个子句则是 C  。如果 C 可以证明自 P ，我们写作 P⊢C。

--------------------------------------------------------------------------------------------------------------------------------

Exercise 2.1.4

从下面的程序中推导【derivation】出 friendly :

happy;friendly:-teacher.
friendly:-teacher,happy.
teacher;wise.
teacher:-wise.

Answer 2.1.4

这需要先推导【derivation】子句 friendly:-teacher 和 teacher 

请注意，这种推导【derivation】不能以线性树【 linear tree】的形式重铸，其中每个归结式【resolvent】都是从前一个归结式【resolvent】和给定子句中获得的，如第 1 章所示。这是因为某些子句是不确定的（有超过一个的正文字【positive literal】）。 

--------------------------------------------------------------------------------------------------------------------------------

Meta-theory

证明命题逻辑中的归结法【propositional resolution】是健全的【sound】是很容易的：您必须证实两个输入子句的每个模型，都是其归结式【resolvent】的模型。 在我们前面的例子中，married;bachelor:-man,adult 和 has_wife:-man,married （输入子句）的模型，必须也是  has_wife;bachelor:-man,adult（归结式）的模型。现在，被归结的文字【the literal resolved upon】（在本例中指的是 married）要么被赋真值 true ，要么被赋真值 false 。

##输入子句
married;bachelor:-man,adult.
has_wife:-man,married.
##归结
has_wife;bachelor:-man,adult

在第一种情况下（married = true ）， has_wife:-man,married 的每个模型也是 has_wife:-man 的模型，而对于 married;bachelor:-man,adult ，由于 married = true ，其真值必然为 true；

在第二种情况下（married = false ）， married;bachelor:-man,adult 的每个模型也是 bachelor:-man,adult 的模型，而对于 has_wife:-man,married ，由于 married = false ，其真值必然为 true。

在这两种情况下，这些模型都是归结式【resolvent】的一个子子句【subclause】的模型，这意味着它们也是归结式【resolvent】本身的模型。

一般来说，证明完备性【completeness】比证明健全性【soundness】更复杂。更糟糕的是，证明归结法【resolution】的完备性是不可能的，因为归结法【resolution】根本就不完备！让我们以 a:-a 子句为例，该子句也被称为重言式【tautology】：它在任何解释【interpretation】下都是 true 。因此，任意程序 P 的任何模型也都是它的模型，因此 P⊨ a:-a 对于任何程序 P 都成立。如果归结是完备的，那么就有可能从某个程序 P 中推导【derive】出子句 a:-a ，其中文字 a 甚至在程序 P 中都不曾出现过！

然而，这并不一定是坏事，因为尽管重言式【tautology】可以从任何子句集【set of clauses】中推断得出，但它们并不是很有趣。归结法【Resolution】解决的是 “子句 C 是程序 P 的逻辑结论【 logical consequence 】吗？”， 而不是“程序 P 的逻辑结论【 logical consequence 】是什么？”这一问题，使得引导推理过程成为可能。我们将看到，虽然归结法【resolution 】不能产生关于某一子句集【set of clauses】的每个逻辑结论【logical consequence】，但是归结法【resolution 】总是可以确定某一特定的子句是否是某一子句集【set of clauses】的逻辑结论【logical consequence】，就这个意义而言，它是完备的【complete】。

这个思想类似于数学中的一种证明技巧，叫做“归谬法【reduction to the absurd】”。假设现在子句 C 只由一个正文字 a 组成（即一个只有子句头 a 而没有子句体的子句），我们想知道 P⊨ a 是否成立，即是否程序 P 的任意模型也是 a 的模型。那么如何校验一个解释【interpretation 】是否是 a 的模型呢？当且仅当该模型不是  :-a 的模型时，那么该模型就是 a 的模型。因此，当且仅当没有一种解释【interpretation 】是 :-a 和  P 二者的模型，那么我们可以说 P 的每个模型就都是 a 的模型。 换句话说，当且仅当  :-a 和  P 是相互不一致的【inconsistent 】（即没有一个公共模型），那么 a 就是 P 的一个逻辑结论【logical consequence】。因此，校验 P⊨ a 是否成立，等价于校验 P∪ { :-a }  是否不一致。

当且仅当陈述集【set of statements】没有模型时，那么该陈述集【set of statements】就是不一致的，即所有的陈述的真值不可能同时为 true 。

这相当于说所有这些语句【sentences】的合取【conjunction】是一个矛盾【contradiction】。

也相当于说矛盾【contradiction】是该语句集【set of sentences】的逻辑结论。

所有这些意味着：

用归结来表明一个集是不一致的：简单地从语句【sentences】开始，将其放入子句【clauses】，然后推导【derive】出空子句！（反过来表明，这些子句来自的原始公式【original formula】 F 是一个矛盾【contradiction】）

或者：如果该集合已经是一堆子句：那么只需推导出空子句！ （反过来，这表明子句来自的原始公式 F 是矛盾的。

https://math.stackexchange/questions/2210460/how-do-i-prove-inconsistency-in-fol

归结法【Resolution 】提供了一种校验这种情况的方法。 请注意，由于不一致【inconsistent 】的子句集【set of clauses】没有模型，因此它自然而然地满足了这样一个条件：它的任何模型都是任何其他子句的模型；因此，不一致的子句集【set of clauses】将所有可能的子句作为其逻辑结论。特别是谬子句【absurd clause】或空子句【empty clause】（用◻来表示），是不一致的子句集【set of clauses】的逻辑结论。反之，如果◻是子句集的逻辑结论，那么该子句集必然不一致。现在，如果子句集 P 是不一致的，那么总有可能通过归结【resolution】推导出◻，从这种意义上来说，归结法【resolution】是完备的。由于归结【resolution】是健全的，我们已经知道如果我们可以推导出◻，那么输入子句一定是不一致的。 所以我们得出结论：如果通过归结，可以从程序 P 与 :-a 推导出空子句【empty clasue，即◻ 】，那么 a 就是程序 P 的逻辑结论。这个过程称为反驳证明/反证【proof by refutation】，归结也被称为反证完备【refutation complete】。

注 ◻ 被称为空子句，因为其子句头和子句体均是空的，因此它无法被任意解释【interpretation】所满足。is called the 

logic - Is resolution complete or only refutation-complete? - Computer Science Stack Exchange

这种证明方法可以推广到 B 不是单个原子【single atom】的情况。 例如，让我们通过规则来校验 a:-a 是一个重言式【tautology】，即是任何子句集的逻辑结论。 从逻辑上讲，这个子句等价于“a or not a”，对其取反得到“not a and a”，它由两个单独的子句表示： :-a 和 a。 由于我们可以在不使用任何其他子句的情况下，在单个归结步骤下，由这两个子句推导出空子句【empty clause】，因此我们实际上已经证明了 a:-a 是空子句集【 empty set of clauses】的逻辑结论，因此它是重言式。

Exercise 2.1.5 

反证 friendly:-has_friends 是下列子句的逻辑结论：

happy:-has_friends.
friendly:-happy.

Answer 2.1.5 

 friendly:-has_friends 的取反正由于两个子句组成：:-friendly 和 has_friends。总之，这四个子句是不一致的：

最后，我们提到虽然归结【resolution 】总是可以用来证明子句集的不一致，但它并不总是适合证明相反的情况，即证明子句集的一致性。 例如，我们知道 a 不是 a:-a 的逻辑结论。 然而，如果我们试图证明 :-a 和 a:-a 的不一致性（应该失败），我们会陷入到归结的不断应用中！ 原因当然是系统中存在一个循环：将归结应用于 :-a 和 a:-a 会再次产生 :-a。 在这种简单的情况下，很容易校验出循环的存在：只需维护一个先前推导出的子句【derived clauses】的列表，不要继续处理先前推导出的子句。

然而，正如我们即将在后面看到的，这在完整子句逻辑【full clausal logic】的一般情况下是不可能的，完全子句逻辑【full clausal logic】在关于“ B 是否是 A 的逻辑结论”这一问题上是半可判定的【semi-decidable】：如果证明存在的话，那么有一种算法，它可以在有限的时间内推导出该证明，但是如果该证明不存在的话，对于任意的 A 和 B ，该算法无法停止并返回“no”。其原因是，完整子句逻辑【full clausal logic】的解释【interpretations】通常是无限的。因此，一些 Prolog 程序可能会永远循环（就像某些 Pascal 程序一样）。有人可能会建议，应该可以通过检查源代码，就可以校验出程序是否会无限循环，但是，正如艾伦·图灵（Alan Turing）所指出的，这通常是不可能的（即著名的停止问题）。也就是说，您可以编写程序来检查程序的终止，但对于任何此类终止检查程序，您可以编写一个不会自行终止的程序！

Tip

prop_atom(married).
prop_atom(bachelor).
prop_atom(man).
prop_atom(adult).


% Propositional atoms are trivially ground
ground_atom(A):-prop_atom(A).

本文标签： 子句逻辑背景理论