計算機邏輯

計算機邏輯是邏輯領域和計算機科學領域之間的重疊部分。 該主題基本上可以分為三個主要領域：理論基礎和分析；使用計算機技術來幫助邏輯學家；將邏輯概念用于計算機應用等。

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

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

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

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

• 范疇論代表了一種強調結構之間關系的數學觀點。 它與計算機科學的許多方面密切相關：編程語言的類型系統、轉換系統理論、編程語言模型和編程語言語義理論。

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

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