计算机科学家逻辑/导论

导论

虽然逻辑自亚里士多德和麦加拉（公元前 430-360 年）以来一直在发展和研究，但我们想关注数学逻辑的发展，哥特弗里德·莱布尼茨可以被认为是其创始人（概念符号，1879）。这是逻辑第一次以完全形式化的语言出现；当然，莱布尼茨和布尔等人为逻辑的 формализация 做出了贡献，但正是弗雷格彻底引入了 формализация 和演绎的概念。这方面对计算机科学特别重要，因为在计算机科学中，演绎过程的自动化正在被研究。现代数学逻辑的发展伴随着数学的深刻危机：在 19 世纪末和 20 世纪初，集合论和算术的公理化一直是数学研究的重点，在 1910-1913 年，怀特海德和罗素出版了他们的《数学原理》，试图在形式逻辑的基础上形式化整个数学，这基本上是弗雷格给出的逻辑。这种形式化使得避免当时讨论的许多矛盾成为可能。然而，在 1931 年，库尔特·哥德尔在他的著名不完备性定理中证明，在给定其一致性的情况下，形式化算术的方法不可能是完整的。重要的是要注意，在 20 世纪 30 年代，理论计算机科学的基础被奠定：艾伦·图灵发表了他关于理论机器和可计算性的工作，阿隆佐·丘奇发展了他的 $\lambda$ -演算，斯蒂芬·克莱尼发展了递归理论的基础。

在本导论的其余部分，我们将直接跳入逻辑在现代计算机科学中的应用。对逻辑史感兴趣的读者请参考本导论结尾的参考书目部分。

编程

在过去十年中，事实证明，计算机化系统是先进技术的基石。软件存在于现代住宅的几乎所有设备中，包括我们的汽车，更不用说飞机或武器了。不用赘述，很明显，对于大多数（如果不是全部）应用而言，系统的健壮、安全和正确行为是强制性的。为了实现这一点，人们普遍认为，只有在硬件和软件开发的整个过程中应用形式化方法才有可能。下面我们将简要介绍一些逻辑的使用已被证明极其有用的任务。

抽象数据类型

为了定义数据类型并为其推导出有效的实现，抽象数据类型定义的概念至关重要。其思想是定义数据类型的抽象属性，而不是给出特殊的实现。一个非常简单的例子是定义一个堆栈：设 $\Sigma$ 为一个字母表。为了定义一个在 $\Sigma$ 上的堆栈 $S$ ，我们假设 $clear$ 是一个零元函数，我们定义堆栈的以下属性

{\begin{matrix}clear\in S\\\forall s\in S\;\forall x\in \Sigma \;(push(s,x)\in S)\\\forall s\in S\;(s\neq clear\Rightarrow pop(s)\in S)\\\forall s\in S\;(s\neq clear\Rightarrow top(s)\in \Sigma )\\\forall s\in S\;(empty(s)\in \{true,false\})\\\end{matrix}}

因此，我们有函数 $clear,push$ 和 $pop$ ，它们生成栈和谓词 $empty$ ，此外，我们需要关于 $push$ 操作的以下属性。

{\begin{matrix}\forall s\in S\;\forall x\in \Sigma \;(push(s,x)\neq clear)\\\forall s\in S\;\forall x,y\in \Sigma \;(push(s,x)=push(s,y)\Rightarrow x=y)\\\forall s,t\in S\;\forall x\in \Sigma \;(push(s,x)=push(t,x)&\Rightarrow s=t)\\\end{matrix}}

我们还需要给出关于函数组合的属性

{\begin{matrix}\forall s\in S\;\forall x\in \Sigma &(top(push(s,x))=x\land pop(push(s,x))=s)\\\forall s\in S\;\forall x\in \Sigma &(empty(push(s,x))=false)\\&empty(clear)=true\\\end{matrix}}

上述公式说明了我们希望栈具有的属性。显然，它不包含任何关于如何实现此类数据类型的提示。实际上，此规范旨在解决其他问题，例如

规范是否正确？即，是否存在一个集合 $S$ ，以及给定的操作，使得上面的公理成立？
规范是否完整？即，公理是否蕴含了我们直觉上认为栈应该具有的所有属性？是否存在集合 $S$ 不符合我们的预期？

读者可能已经注意到，公理只不过是谓词逻辑中的公式，也就是说，所有变量如 $x$ 或 $s$ 以及所谓的量词 $\forall$ 和 $\exists$ 被使用。上述两个问题，即正确性和完整性，是逻辑中形式系统设计的核心主题。证明这些性质往往很困难且成本高昂，但另一方面，逻辑系统的明显优势之一是这些性质可以被形式地证明。在本课程的主要部分，我们将明确地处理这些问题。

程序开发

有许多尝试来定义方法，这些方法允许程序的开发以及对其正确性的形式化论证。我们将用一个玩具示例来简要说明。假设以下简单的程序包含一个循环，并且假设它有一个整数数组

   max := a(1);
   do i = 2,n
   if a(i) > max then max := a(i)
   end

为了理解执行此程序时发生的情况，以下所谓的循环不变式很有帮助

$\forall j:1\leq j\leq i\Rightarrow max\geq a(j)$

这意味着，对于每个 $i$ 的值，即在 do 循环中 if 语句的每次执行之前和之后，上述公式都是有效的。现在假设循环最后一次执行，因此 $i$ 在执行循环体后的值为 $n$ ，可以得出结论，max 包含数组的最大值

$\forall j:1\leq j\leq n\Rightarrow max\geq a(j)$

程序开发的另一个重要问题是程序规范。为了给出上面用于查找数组最大值的程序的形式规范，可以使用以下逻辑公式

$\forall S\;\forall m\;max(S,m)\Leftrightarrow (S\neq \emptyset \Rightarrow (m\in S\land \forall x\;(x\in S\Rightarrow m\geq x)))$

注意，在此规范中 $S$ 被假定为一个集合。还没有决定是否必须通过数组来实现这一点。

另一方面，逻辑不仅可以用于规范，还可以作为程序本身使用。以下是计算值列表的最大值的逻辑程序。列表表示为 [ head.tail ]，其中 head 表示列表的前部元素，tail 表示列表的其余部分，nil 表示空列表。

 
   max([m.nil], m) <-  .
   max([head.tail], m)    <-  max([tail], m), 
                              head < m. 
   max([head.tail], head) <-  max([tail], m), 
                              head >= m.

人工智能

人工智能 (AI) 研究中最古老的子学科之一是自动定理证明。在早期，一些人对使用定理证明器作为各种不同任务的通用问题解决器持乐观态度，例如动作规划、知识表示或程序验证。现在很清楚，对于专门的任务，需要定制的推理系统。在本节中，我们将评论定理证明，旨在证明数学定理和知识表示。这个想法可以看作是对戈特弗里德·威廉·莱布尼茨 (1646 - 1716) 想法的回归，他早在那个时候就梦想对数学进行形式化，甚至自动化。

最近的成功是罗宾斯猜想的证明，它甚至登上了《纽约时报》。有关详细信息，请参见http://www-unix.mcs.anl.gov/~mccune/papers/robbins/。1933 年，E. V. Huntington 提出了布尔代数的以下基础

    x + y = y + x.                      
                      [commutativity]
    (x + y) + z = x + (y + z).          
                      [associativity]
    n(n(x) + y) + n(n(x) + n(y)) = x.   
                      [Huntington equation]

此后不久，Herbert Robbins 推测，Huntington 方程可以用一个更简单的方程代替

    n(n(x + y) + n(x + n(y))) = x.      
                      [Robbins equation]

罗宾斯和亨廷顿找不到证明，这个问题后来被塔斯基和他的学生研究。解决罗宾斯问题的证明于 1996 年 10 月 10 日由定理证明器 EQP 找到。EQP 在许多方面类似于更著名的程序http://www.mcs.anl.gov/AR/otter/。主要区别在于 EQP 具有结合-交换 (AC) 统一，仅限于等式逻辑，并提供更多参数化策略。有关详细信息，请参见http://www.mcs.anl.gov/~mccune/papers/33-basic-test-problems/。

知识表示

在许多人工智能中，知识的表示和操作是一项核心任务。为此，已经发明了大量面向图形的形式主义。

这种图形符号的非正式语义指出，人和动物都是哺乳动物，并且人具有国籍和年龄，而动物具有年龄而没有国籍。对这种形式主义语义的更深入研究将表明，这只不过是对以下谓词逻辑公式集的图形表示
$\forall x(man(x)\Rightarrow mammal(x))$
$\forall x(animal(x)\Rightarrow mammal(x))$
$\forall x(man(x)\Rightarrow \exists y\;age(x,y))$
$\forall x(man(x)\Rightarrow \exists y\;nationality(x,y))$
$\forall x(mammal(x)\Rightarrow \exists y\;age(x))$

另请参阅：Gellrich/Gellrich: Mathematik (1) - Schaltalgebra
例子

问题

问题 1 (介绍)

在一个刑事案件中，以下事实被证明

三人 X、Y、Z 中至少一人有罪。
如果 X 有罪而 Y 无罪，那么 Z 有罪。

这些情况不足以指控其中一人，但可以肯定地说，两人中至少一人有罪。这两者是谁？

问题 2 (介绍)

以下三段论哪些是有效的？请说明你的答案的理由，或者给出反例。

所有 $M$ 都是 $P$ ，一些 $S$ 不是 $M$ ，那么：一些 $S$ 是 $P$ .
所有 $M$ 都是 $P$ ，一些 $S$ 不是 $M$ ，那么：一些 $S$ 不是 $P$
所有 $P$ 都是 $M$ ，一些 $S$ 不是 $M$ ，那么：一些 $S$ 不是 $P$ 。

问题 3（引言）

在一个会议上，有 100 位政治家互相讨论。他们每个人要么是腐败的，要么是非腐败的。以下是已知的事实

至少有一位政治家是非腐败的。
在每两个政治家的配对中，至少有一位是腐败的。有多少政治家是腐败的，有多少是非腐败的？

问题 4（引言）

人类学家阿伯克龙比踏上骑士与混蛋岛时，从未有过的沮丧感涌上心头。他知道这个岛上住着非凡的人：骑士总是说真话，混蛋则总是说假话。阿伯克龙比也知道，他必须找到一个朋友才能体验到一些东西。他必须找到一个可以信任其所说的话的人。因此，他向岛上遇到的前三个人询问如何找到一个骑士。阿伯克龙比首先问亚瑟：“伯纳德和查尔斯都是骑士吗？”亚瑟回答：“是的，他们都是！”然后阿伯克龙比问：“伯纳德是骑士吗？”令他大吃一惊的是，他得到了回答：“不是！”“查尔斯是骑士还是混蛋？”推断你的答案并说明原因。

问题 5（引言）

一个小岛上只有 100 个居民。每个居民要么总是说真话，要么总是说谎。有一天，一位研究人员来到岛上，按顺序询问了岛民。第一个说：“我们中间至少有一个说谎者。”第二个说：“我们中间至少有两个说谎者。”等等。最后一个最后说：“这个岛上 100 个都是说谎者。”实际上有多少说谎者？一年后，研究人员来到另一个有 99 个居民的岛屿。在一次访谈中，这些岛民的谈话内容与第一个岛屿上的居民完全一致，也就是说，第 $n$ 个居民说：“这里至少有 $n$ 个说谎者。”关于这个岛屿，你能说些什么？

问题 6（引言）

在一个村庄里，牧师在周日解释说：“有人向我坦白，我们村庄里有人不忠。然而，坦白的秘密禁止我说出名字。不过，如果我们按以下步骤进行，你们还是会知道他们是谁：任何确信自己丈夫不忠的女人，将在接下来的晚上将他赶出家门。”问题是，每个女人都知道其他每个人的丈夫的情况，但不知道自己丈夫的情况。第二天早上，牧师走过街道；没有一个人被赶走。第二天，他也什么都没看到。但在第 100 英亩的地方，他看到了被妻子赶出家门的男人。有多少人？

问题 7（引言）

有一家旅馆，有无数个房间，编号为 0、1、2、…… 所有房间都是空着的。现在，一辆 $\omega$ 层的公共汽车来了，每层都有 $\omega$ 个座位。如何将所有乘客安排在旅馆里？

直到计算机科学家逻辑