prolog解析如何使用反证法？

Question

我正在学习 prolog，我对 prolog 使用矛盾证明的说法感到困惑：

解析证明过程利用了一种被称为“归谬法”的技术：假设要证明的公式是假的，并证明这会导致矛盾，从而证明要证明的公式实际上是正确的。

他们展示了以下证明图（基于前面一节建立的规则和事实）：

但如果我倒着读这些步骤，那就是一个简单直接的证明：

/* axiom: tottenham_court_road is connected to leicester_square by northern road */
connected(tottenham_court_road, leicester_square, northern)

/* therefore it's connected to something on some road */
connected(tottenham_court_road, W, L)

/* being connected to something also means it's nearby */
nearby(X,Y):-connected(X,Y,L)

/* Therefore tottenham_court_road is near something */
nearby(tottenham_court_road, W)

这是如何用反证法证明的呢？为什么这是一个比公理链式推理更有用的框架？

Answer 1

喇叭条款

\n

Horn 子句是最多具有一个正文字的析取，其中所有变量都在整个公式上隐式普遍量化。例如，

\n

\xc2\xacfather(X,Y) \xe2\x88\xa8 \xc2\xacfather(Y,Z) \xe2\x88\xa8 grandfather(X,Z)

\n

是一个霍恩子句。由于 \xc2\xac \xce\ xb1 \xe2\x88\xa8 \xc2\xac \xce\xb2相当于 \xc2\xac( \xce\xb1 \xe2\x88\xa7 \ xce\xb2 )，并且 \xc2 \xac \xce\xb1 \xe2\x88\xa8 \xce\xb2相当于\xce\xb1 \xe2\x86\x92 \xce\xb2， Horn 子句可以写为：

\n

  \xc2\xacfather(X,Y) \xe2\x88\xa8 \xc2\xacfather(Y,Z) \xe2\x88\xa8 grandfather(X,Z)\n\xe2\x89\xa1 \xc2\xac(father(X,Y) \xe2\x88\xa7 father(Y,Z)) \xe2\x88\xa8 grandfather(X,Z)\n\xe2\x89\xa1 father(X,Y) \xe2\x88\xa7 father(Y,Z) \xe2\x86\x92 grandfather(X,Z)\n

\n

或者，等价地，如：

\n

grandfather(X,Z) \xe2\x86\x90 father(X,Y) \xe2\x88\xa7 father(Y,Z)\n

\n

\n

• 由单个正文字组成的 Horn 子句称为事实。例如，father(adam,cain) \xe2\x88\xa8 \xe2\x8a\xa5可以写成father(adam,cain) \xe2\x86\x90 \xe2\x8a\xa4， 是事实。

  \n
\n

• 没有正文字的 Horn 子句称为目标（也称为查询）。例如，\xe2\x8a\xa5 \xe2\x88\xa8 \xc2\xacfather(adam,cain)，可以写成\xe2\x8a\xa5 \xe2\x86\x90 father(adam,cain)，是一个目标。

  \n
\n

• \xe2\x8a\xa5 \xe2\x86\x90 \xe2\x8a\xa4 形式的 Horn 子句称为矛盾。例如，目标\xe2\x8a\xa5 \xe2\x86\x90 father(adam,cain)与事实的解决father(adam,cain) \xe2\x86\x90 \xe2\x8a\xa4会产生解决方案\xe2\x8a\xa5 \xe2\x86\x90 \xe2\x8a\xa4。\xe2\x86\x90 的左侧文字为正，右侧文字为负。因此，\xe2\x86\x90 两侧的两个统一文字可以通过解析取消。

  \n
\n

• 不是目标子句的霍恩子句称为确定子句。

  \n
\n

• 一组确定的子句称为逻辑程序。

  \n
\n

\n

在逻辑编程中，常量文字 \xe2\x8a\xa5 和 \xe2\x8a\xa4 经常被省略。通常，事实写为\xce\xb1 \xe2\x86\x90 ，目标写为 \xe2\x86\x90 \xce\xb1，矛盾写为 \xe2\x86\x90 。

\n

Horn 子句表达了具有非常有用的属性的 FOL 子集（例如，独特的最小模型和相对较低的计算复杂性）。事实上，逻辑编程和 Prolog 都是建立在 Horn 子句之上的。

\n

反证法

\n

考虑以下逻辑程序（带有编号子句）：

\n

(1) father(adam,abel) \xe2\x86\x90\n(2) father(adam,cain) \xe2\x86\x90\n(3) father(adam,seth) \xe2\x86\x90\n(4) father(seth,enos) \xe2\x86\x90\n(5) grandfather(X,Z) \xe2\x86\x90 father(X,Y) \xe2\x88\xa7 father(Y,Z)\n

\n

问题以挪士的祖父是谁？（也就是说，有一个人是以诺斯的祖父，我们想知道这个人是谁）可以用公式来表达\xe2\x88\x83W.grandfather(W,enos)。显然，该公式不是霍恩子句。然而，为了通过反证法证明该公式，我们必须考虑它的否定：

\n

  \xc2\xac\xe2\x88\x83W.grandfather(W,enos)\n\xe2\x89\xa1 \xe2\x88\x80W.\xc2\xacgrandfather(W,enos)\n\xe2\x89\xa1 \xe2\x88\x80W.[\xe2\x8a\xa5 \xe2\x88\xa8 \xc2\xacgrandfather(W,enos)]\n\xe2\x89\xa1 \xe2\x8a\xa5 \xe2\x86\x90 grandfather(W,enos)\n\xe2\x89\xa1 \xe2\x86\x90 grandfather(W,enos)\n

\n

这确实是霍恩条款（或更准确地说，目标条款）。

\n

因此，如果逻辑程序 (1)-(5) 是一致的并且\xe2\x88\x83W.grandfather(W,enos)对于该程序来说是正确的，那么目标\xe2\x86\x90 grandfather(W,enos)一定会导致矛盾（并且绑定到通用变量的常量W必须是问题所需的答案）：

\n

\xe2\x86\x90 grandfather(W,enos)   (5) grandfather(X,Z) \xe2\x86\x90 father(X,Y) \xe2\x88\xa7 father(Y,Z)\n  |                         |\n  +-------------------------+ {X=W, Z=enos}                 \n  |\n\xe2\x86\x90 father(W,Y) \xe2\x88\xa7 father(Y,enos)   (3) father(adam,seth) \xe2\x86\x90\n  |                                  |\n  +----------------------------------+ {W=adam, Y=seth} \n  |\n\xe2\x86\x90 father(seth,enos)   (4) father(seth,enos) \xe2\x86\x90\n  |                       |\n  +-----------------------+ {}\n  |\n\xe2\x86\x90 [contradiction]\n

\n

Horn 子句由于其非常好的属性而在各种应用中都很有用：两个 Horn 子句的解析是一个新的 Horn 子句，而目标子句和确定子句的解析是一个新的目标子句。

\n

Horn 子句和 Prolog

\n

在 Prolog 中，连接词\xe2\x88\xa7被替换为,，连接词\xe2\x86\x90被替换为:-（除了在事实中，连接词被省略，以及在目标中，顶级提示?-隐式代表\xe2\x86\x90）。

\n

\n

“在逻辑中，这是通过将陈述写成带有空结论的规则来实现的，即，其前提的真实性将导致虚假的规则”

\n

\n

带有空结论的子句只不过是 \xe2\x86\x90 \xce\xb1形式的目标，它相当于 \xe2\x8a\xa5 \xe2\x86\x90 \xce\xb1。因此，如果前提\xce\xb1为真：

\n

  \xe2\x8a\xa5 \xe2\x86\x90 \xce\xb1\n\xe2\x89\xa1 \xe2\x8a\xa5 \xe2\x86\x90 \xe2\x8a\xa4\n\xe2\x89\xa1 \xe2\x8a\xa5 \xe2\x88\xa8 \xc2\xac\xe2\x8a\xa4\n\xe2\x89\xa1 \xe2\x8a\xa5      [falsity]\n

\n

\n

因此，符号“?-”和“:-”实际上是等价的。如果解析导致空规则，则发现矛盾，其中前提始终为真（因为不存在），但结论始终为假。

\n

\n

由于符号?-和:-都用来代替\xe2\x86\x90，显然它们是等价的。特别是，该符号?-仅隐式使用（当在顶级提示中键入查询时）。在 Prolog 的某些实现中，程序源代码中的目标子句会在加载该程序时自动执行。例如，当以下程序加载到 SWI-Prolog 中时，文本Hi Alfred!将写入当前输出：

\n

user('Alfred').                             % user('Alfred') \xe2\x86\x90\n:- user(Name), format('Hi ~w!~n', [Name]).  % \xe2\x86\x90 user(Name), format('Hi ~w!~n', [Name]).\n

\n

空规则只是矛盾的另一个名称（即 ，\xe2\x8a\xa5 \xe2\x86\x90 \xe2\x8a\xa4通常简单写为\xe2\x86\x90）。当然，空规则的前提始终为真（\xe2\x8a\xa4），其结论始终为假（\xe2\x8a\xa5）。

\n