數理邏輯之 入門及參考資料推薦

打算發表一系列關于數理邏輯基礎的小文章，希望對一部分讀者有用。

數理邏輯又稱符号邏輯、理論邏輯。它既是數學的一個分支，也是邏輯學的一個分支。是用數學方法研究邏輯或形式邏輯的學科。其研究對象是對證明和計算這兩個直覺概念進行符号化以後的形式系統。數理邏輯是數學基礎的一個不可缺少的組成部分。雖然名稱中有邏輯兩字，但并不屬于單純邏輯學範疇。（百度百科）

也許看了上述定義你依然不知道學習計算機技術和數理邏輯之間有什麼關系。簡單的說，軟體形式化方法已被廣泛關注（你可以搜一下這方面的論文，十分多）。規範語言、定理證明器、模型檢測器正被企業正常地應用。而數理邏輯是所有這些技術的基礎。現在數理邏輯是計算機科學與技術專業的一門重要的基礎課程。

數理邏輯基本的概念涉及：

1。命題邏輯

（包括命題、自然演算、相繼式；

合取規則、雙重否定規則、蘊含消去規則、MT規則、蘊含引入規則、析取引入和消去規則、copy規則、否定規則、否定引入規則、

MT導出規則、雙重否定導出規則、PBC導出規則、排中律導出規則；

合式公式及其文法樹和字元串、合式公式的高度、重言式；

範式的語意等值、可滿足性、有效性；

合取範式、析取子句、Horn子句；

逼迫規則）

2。謂詞邏輯，是為了解決命題邏輯的局限性

（包括謂詞表達語句、謂詞演算公式、函數符号；

謂詞公式三個集合、語言的項、謂詞公式文法樹、自由變量和限制變量、代換；量詞的等價；

謂詞邏輯的語意、語意推導、語意相等；

謂詞邏輯公式的不可判定性；

謂詞邏輯的表達能力、一階謂詞邏輯、存在二階邏輯、全稱二階邏輯）

3。如果有時間，稍微說一下形式驗證。

（包括模型檢測；

時态邏輯、線性時态邏輯、計算樹邏輯；

遷移系統、有向圖表示、路徑；

線性時态邏輯間的等價、連接配接詞集）

如果你對這些概念很熟悉或者完全不感興趣，請掠過；否則敬請期待随後的文章。

推薦的參考資料有：

1。面向計算機科學的數理邏輯（第二版）陸鐘萬  科學出版社 2002年1月

2。Logic in Computer Science: Modelling and Reasoning about System,Second Edition,  Michael Huth and Mark Ryan,  Originally Published by Cambridge University Press in 2004.

3。Logic for Mathematicians(Revised Edition)， A. G. Hamilton,  Originally Published by Cambridge University Press in 1978(1988).