計算機邏輯

計算機邏輯是邏輯領(lǐng)域和計算機科學(xué)領(lǐng)域之間的重疊部分。 該主題基本上可以分為三個主要領(lǐng)域：理論基礎(chǔ)和分析；使用計算機技術(shù)來幫助邏輯學(xué)家；將邏輯概念用于計算機應(yīng)用等。

邏輯在計算機科學(xué)中起著基礎(chǔ)性的作用。 一些特別重要的邏輯關(guān)鍵領(lǐng)域是可計算性理論（以前稱為遞歸理論）、模態(tài)邏輯和范疇論。 計算理論基于邏輯學(xué)家和數(shù)學(xué)家定義的概念，例如 Alonzo Church 和 Alan Turing。 Church 首先使用他的 lambda 可定義性概念證明了算法無法解決的問題的存在。 圖靈首次對所謂的機械過程進(jìn)行了令人信服的分析，庫爾特·哥德爾斷言他發(fā)現(xiàn)圖靈的分析是完美的。此外，邏輯和計算機科學(xué)之間理論重疊的其他一些主要領(lǐng)域是：

• 哥德爾的不完備性定理證明，任何強大到足以表征算術(shù)的邏輯系統(tǒng)都將包含在該系統(tǒng)內(nèi)既不能證明也不能反駁的陳述。 這直接應(yīng)用于與證明軟件完整性和正確性的可行性相關(guān)的理論問題。

• 框架問題是使用一階邏輯表示人工智能代理的目標(biāo)和狀態(tài)時必須克服的基本問題。

• Curry-Howard 對應(yīng)是邏輯系統(tǒng)和軟件之間的一種關(guān)系。 該理論在證明和程序之間建立了精確的對應(yīng)關(guān)系。 特別是，它表明簡單類型 lambda 演算中的項對應(yīng)于直覺命題邏輯的證明。

• 范疇論代表了一種強調(diào)結(jié)構(gòu)之間關(guān)系的數(shù)學(xué)觀點。 它與計算機科學(xué)的許多方面密切相關(guān)：編程語言的類型系統(tǒng)、轉(zhuǎn)換系統(tǒng)理論、編程語言模型和編程語言語義理論。

最早使用人工智能這個術(shù)語的應(yīng)用程序之一是由 Allen Newell、J. C. Shaw 和 Herbert Simon 在 1956 年開發(fā)的邏輯理論家系統(tǒng)。 邏輯定律必須為真的結(jié)論（附加陳述）。 例如，如果給定一個邏輯系統(tǒng)，聲明所有人類都會死，而蘇格拉底是人類，那么有效的結(jié)論是蘇格拉底會死。 當(dāng)然，這是一個微不足道的例子。 在實際的邏輯系統(tǒng)中，語句可能很多而且很復(fù)雜。 人們很早就意識到，這種分析可以通過使用計算機得到顯著的幫助。 邏輯理論家驗證了伯特蘭·羅素和阿爾弗雷德·諾斯·懷特海在他們關(guān)于數(shù)學(xué)邏輯的有影響力的著作《數(shù)學(xué)原理》中的理論工作。 此外，邏輯學(xué)家已經(jīng)利用后續(xù)系統(tǒng)來驗證和發(fā)現(xiàn)新的邏輯定理和證明。

數(shù)理邏輯對人工智能 (AI) 領(lǐng)域的影響一直很大。 從該領(lǐng)域一開始，人們就意識到自動化邏輯推理技術(shù)在解決問題和從事實中得出結(jié)論方面具有巨大潛力。 Ron Brachman 將一階邏輯 (FOL) 描述為評估所有 AI 知識表示形式的指標(biāo)。 沒有比 FOL 更通用或更強大的已知方法來描述和分析信息。 FOL 本身不被用作計算機語言的原因是它實際上太具有表現(xiàn)力，從某種意義上說，F(xiàn)OL 可以輕松表達(dá)任何計算機（無論多么強大）都無法解決的語句。出于這個原因，每種形式的知識表示在某種意義上都是表達(dá)性和可計算性之間的權(quán)衡。 語言表達(dá)能力越強，越接近FOL，越容易變慢，容易死循環(huán)。例如，專家系統(tǒng)中使用的 IF THEN 規(guī)則近似于 FOL 的一個非常有限的子集。 出發(fā)點不是邏輯運算符的任意公式，而是邏輯學(xué)家所說的 modus ponens。 因此，基于規(guī)則的系統(tǒng)可以支持高性能計算，特別是如果它們利用優(yōu)化算法和編譯。邏輯理論的另一個主要研究領(lǐng)域是軟件工程。 基于知識的軟件助手和程序員學(xué)徒程序等研究項目應(yīng)用邏輯理論來驗證軟件規(guī)范的正確性。