係統是由一些產生式規則組成的一種符號處理係統(可能是曆史上第一種這樣的理論)。該理論已經對計算機科學產生了明顯的影響。範式文法都是在思想影響下形成的。
應當注意規範係統的本來形式可以看作為一組證明規則(他曾視這種係統為謂詞邏輯的推廣而建立在係統上的算法(主要由其他學者建立)已經證明與遞歸函數、丁機等等價。一件應注意的事實是,係統以及其各種推廣形式是一種形式語言,這種語言既可用作邏輯語言、程序設計語言,也可用作硬件設計語言。另一件令人感興趣的事實是,規範係統可以看作是並發邏輯的第一個例子,亦即一種邏輯演算,在這種邏輯演算中,可以有同時進行的多種推理過程。這可以從下列的例子看出。
必須注意,雖然和都由在符號表達式上進行的並行操作組成後麵我們將把這些表示式稱作“字”,但它們是不一樣的,在式子中那些操作是彼此獨立的,而在式子中那些操作是彼此相關的。
在下麵我們將說明如何用係統作為程序設計語言和硬件設計語言,我們將提出?04算法的一種推廣形式,這種算法實際上是一種將符號表達式的遞歸函數嵌入通常的1*051算法之中而構成的兩層算法。它類似於60年代初期08561提出的函數算法。這種算法既可以用作程序設計語言,也可以用作硬件設
邏輯與人工智能(詳細摘要)
一、緒言
可以把人工智能看作是對機器模擬包括推理過程的人類智能的研究。這樣,邏輯作為科學,其形式方麵(即其非心理方麵)勻、工智能是密切相關的。我們準備就以卜論題進行討論。
知識表示將人的知識(包拈常識)轉換成適用機器存貯和處理的形式是人智能的(要問題之一)在過去數十年間充分發展的形式方法已被證明這種有用的,甚至不可缺少的用於知識領域的發明。
近年來麥克德莫特和道爾以應用“人工智能”為目的而創立的非單調邏輯為辦和其他學者所感興趣。該邏輯由下述特性所該劃,而這一特性在古典邏輯中顯然是不存在的,即增加前提可能會使原來的結論無效。
邏輯與自動定理證明
原則上,所有的數學命題都可以由一階邏輯表達,這是眾所周知的事實。定理證明的完全自動化在-階邏輯的判定問題是算法可解的情形下(即,存在一個算法,它對任何邏輯公式,可以確定是否成立)應該是能進行的。不幸(或者從國際數學界的立場上,我們應該說“幸虧”)一階邏輯的判定問題不是算法可解的,這已為人們所證明,因而完全自動化是不可能的。
不過,即,算法可作為一種以下述方式證明定理的工具:對一特定的公式類給定公式廠算法可終結,回答“,而當柯時則終結。當然,這是一種廣義的算法還是可能的。早在1958年,王浩就構造了將一個這類算法嵌人其中的程序,用其所編程序在一台第一代計算機上以不到三分鍾的時間證明了羅素等所著《數學原理》前五章中的全部二百多條定理此事見王浩所著《走向機械化數學》。
人們逐漸認識到,經典證明論(即隻證明論)主要注重各種數學理論的一致性證明問題,與自動定理證明無直接聯係。證明論注重證明的結構和性質的研究,原則上與自動定理證明相關,其在自動定理證明中的應用前景是有希望的。
過去十年間得到的扭出時第十問題是否存在算法確定給定的“丟番圖方程”有無整數解否定解的一些肯定結果似乎也是對自動定理證明有用的。鑒於大多數數學問題都可以歸納為某些類為算法可解決的丟番圖方程這一事實,近來“丟番圖理論”上的進展可能與自動定理證明有關。
邏輯與自動程序設計
1947年,在一篇遲至1969年才發表的文章中指出,有可能由自動定理證明這一途徑達到程序設計的自動化。在1969年獨立地提出了想法。他們提議由構造性證明中獲取算法。其思想是.當想要合成一個計算給定的函數的值是一個可計算函數,0是一個自然數的程序時,我們首先構造命題的一個構造性證明,然後從這個證明中提出算法。
近年來人們仍然與該方法剛剛麵世時一樣,認為該方法並非不可行。
邏輯與“人工智能”的基本問題
在“人工智能”的基本題之中,最令人感興趣的是:“機器能思考嗎?”,或者我們應該叫:“是否可能產生:出具有與人類智能相同行為的計算機?”
考慮這個引起激烈爭論的問題時,我們還是先代之以這樣的問題:“是否可能對一個計算機編程使其行為與一個交互係統(即人十計算機)相同”,接下來,我們可以大膽地提出論題:一個交互係統的行為至多等同複雜的機器。