計算機科學家邏輯/導論

導論

雖然邏輯自亞里士多德和麥加拉（公元前 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$ 個座位。如何將所有乘客安排在旅館裡？

直到計算機科學家邏輯