數(shù)理邏輯復習提綱(11級)

1、數(shù)理邏輯 復習提綱（請按照下面的內(nèi)容復習，有問題隨時到我的辦公室答疑）命題邏輯語法的 BNF 范式及其解釋。命題邏輯的可靠性和完全性定理.謂詞邏輯語法的 BNF 范式及其解釋。線性時態(tài)邏輯的語法的的 BNF 范式及其解釋。分支時態(tài)邏輯的語法的的 BNF 范式及其解釋。謂詞邏輯的可靠性和完全性定理.謂詞邏輯的不可判定性Horn formula 的定義及其可滿足性算法..線性和立方 SAT solver 局限性。一階邏輯和高階邏輯在語法和表

2、達能力差別？一階謂詞邏輯的項和公式是如何定義的，寫出他們的 BNF 范式并解釋之。解釋常用的線性時態(tài)邏輯公式的含義。解釋常用的分支時態(tài)邏輯公式的含義。程序的部分正確定性證明規(guī)則。簡單的程序部分正確性證明。了解 Model Checker 和 NuSMV。會用命題邏輯的自然演繹系統(tǒng)規(guī)則推導簡單的命題邏輯公式。會用謂詞邏輯邏的自然演繹系統(tǒng)規(guī)則推導簡單的謂詞邏輯公式。二命題邏輯語法的 BNF 范式及其解釋。| ( ) | ( ) | ( )

3、| ( ) p ? ? ? ? ? ? ? ? ? ? ? ? ?P 代表任意原子命題，：：=右邊的 和每一次出現(xiàn)都表示任何已經(jīng)構(gòu)造好的公式。 ?命題邏輯的可靠性和完全性定理.設 和 是命題邏輯公式。若 成立時， 成立，則是可 1 2 , ,..., n ? ? ? ? 1 2 , ,..., | n ? ? ? ? ? 1 2 , ,..., | n ? ? ? ? ?靠的。若 成立時， 成立，則是完全的。 1 2 , ,..., |

4、 n ? ? ? ? ? 1 2 , ,..., | n ? ? ? ? ?謂詞邏輯語法的 BNF 范式及其解釋。其中 是 1 n 元的謂 1, 2 :: ( ,..., ) | ( ) | ( ) | ( ) | ( ) | ( ) | ( ) n P t t t x x ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? p ? ? ?詞符號， 是 F 上的項，x 是變量。在：：=的右邊， 的每次出現(xiàn)都表示由上述規(guī)則

5、構(gòu)造出來的任意公 i t ?式。線性時態(tài)邏輯的語法的的 BNF 范式及其解釋。:: | ( ) | | ( ) | ( ) | ( ) | ( ) | ( ) | ( ) | ( ) | ( ) | | ( ) p X F G U W R ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?? ? ? ? ? ? ?其中 P 是取自某原子集 atoms 的任意命題原子。連接詞 X,F,G,U,R 和 W 稱為時態(tài)連接詞

6、。分支時態(tài)邏輯的語法的的 BNF 范式及其解釋。謂詞邏輯比命題邏輯有更強大的表達能為，它有謂詞，函數(shù)符號和量詞符號。但這是以犧牲有效性，可滿足性和可證明性的不可判定性為代價的。而謂詞不能表達可達性，高階邏輯可以表達，但高階邏輯在像完備性和緊密性這樣的典型結(jié)果可能很快就不再成立。而且一個樸素的高階邏輯在元邏輯級上可能是不相容的。一階謂詞邏輯的項和公式是如何定義的，寫出他們的 BNF 范式并解釋之。項定義如下：任何變量都是項；若 F 是零元

7、函數(shù)，則 c 是項。 c?若 是項，且 f F 的元 n>0，則 是項。 1, 2,..., n t t t ? 1, 2 ( ,..., ) n f t t t沒有其它形式的項。用 backus naur 范式，可以寫：，其中 x 取遍 F 中的零元函數(shù)符號，f 取遍 F 中的元 n>0 的符 1, 2 :: | | ( ,..., ) n t x c f t t t ?號。解釋常用的線性時態(tài)邏輯公式的含義。解釋常用的分支

8、時態(tài)邏輯公式的含義。程序的部分正確定性證明規(guī)則。? ? ? ?? ? ? ?? ? ? ?1 21; 2C C Composition C C? ? ? ?? ?? ? ? ? [ / ] Assignment E x x E ? ? ?? ? ? ?? ? ? ?? ? ? ?1 2 _ { 1}B C B C Lf statement ifB C else? ? ? ?? ?? ? ?? ? ? ?? ? ? ?_ { }B C P

9、artial while whileB C B? ?? ??? ?? ? ? ?? ? ? ?' '' '| ; ;| ImAR AR C pliedC? ? ? ? ? ?? ?? ? ? ?簡單的程序部分正確性證明。了解 Model Checker 和 NuSMV。NuSMV(有時簡稱 SMV)提供描述一種用圖來描述的模型的語言，而且可以直接驗證基于這個模型的 LTL(或 CTL)公式的有效性。SMV