打算發表一系列關於數理邏輯基礎的小文章，希望對一部分讀者有用。
數理邏輯又稱
符號邏輯
、理論邏輯。它既是數學的乙個分支，也是邏輯學的乙個分支。是用
數學方法
研究邏輯或形式邏輯的學科。其研究物件是對證明和計算這兩個直觀概念進行符號化以後的形式系統。數理邏輯是
數學基礎
也許看了上述定義你依然不知道學習計算機技術和數理邏輯之間有什麼關係。簡單的說，
軟體形式化方法已被廣泛關注（你可以搜一下這方面的**，十分多）。規範語言、定理證明器、模型檢測器正被企業常規地應用。而數理邏輯是所有這些技術的基礎。現在數理邏輯是電腦科學與技術專業的一門重要的基礎課程。
數理邏輯基本的概念涉及：
1。命題邏輯
（包括命題、自然演算、相繼式；
合取規則、雙重否定規則、蘊含消去規則、mt規則、蘊含引入規則、析取引入和消去規則、copy規則、否定規則、否定引入規則、
mt匯出規則、雙重否定匯出規則、pbc匯出規則、排中律匯出規則；
合式公式及其語法樹和字串、合式公式的高度、重言式；
正規化的語意等值、可滿足性、有效性；
合取正規化、析取子句、horn子句；
逼迫規則）
2。謂詞邏輯，是為了解決命題邏輯的侷限性
（包括謂詞表達語句、謂詞演算公式、函式符號；
謂詞公式三個集合、語言的項、謂詞公式語法樹、自由變數和約束變數、代換；量詞的等價；
謂詞邏輯的語意、語意推導、語意相等；
謂詞邏輯公式的不可判定性；
謂詞邏輯的表達能力、一階謂詞邏輯、存在二階邏輯、全稱二階邏輯）
3。如果有時間，稍微說一下形式驗證。
（包括模型檢測；
時態邏輯、線性時態邏輯、計算樹邏輯；
遷移系統、有向圖表示、路徑；
線性時態邏輯間的等價、連線詞集）
如果你對這些概念很熟悉或者完全不感興趣，請掠過；否則敬請期待隨後的文章。
推薦的參考資料有：
1。面向電腦科學的數理邏輯（第二版）陸鐘萬 科學出版社 2023年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).
數理邏輯之 正規化
今天開始說正規化。先介紹幾個概念。語義等值 令 和 是命題邏輯公式，我們稱 和 語義等值當且僅當 且 成立。記為 可滿足公式 給定命題邏輯公式 我們說 是可滿足的，如果存在 的一次求值使得 取值 true.文字 文字l 是指命題原子p或 p。l p p 析取子句 析取子句 d是若干個文字的析取 d ...
數理邏輯之 horn公式
horn公式，中文名一般翻譯成 霍恩公式 也是正規化的一種。horn原子有三 p t p horn原子分別是底公式 頂公式和命題原子。horn原子合取後的蘊含稱為horn字句 a p p a c a p horn子句 繼續合取就是horn公式 h c c h horn公式下面的都是horn公式例子 ...
數理邏輯之 自然演算規則（三）
截止到前文數理邏輯之 自然演算規則 二 我們已經學習了四種7個命題邏輯的自然演算規則，分別是合取規則 雙重否定規則 蘊含消去規則 mt規則。接下來我們要學習的規則不僅從規模上看起來比前面的要大，理解和使用上也提公升了難度。第五種規則叫 蘊含引入規則 蘊含引入規則會基於前提進行合理的假設提出，並根據合...