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

數(shù)理邏輯復習提綱（請按照下面的內容復習，有問題隨時到我的辦公室答疑）命題邏輯語法的BNF范式及其解釋。命題邏輯的可靠性和完全性定理.謂詞邏輯語法的BNF范式及其解釋。線性時態(tài)邏輯的語法的的BNF范式及其解釋。分支時態(tài)邏輯的語法的的BNF范式及其解釋。謂詞邏輯的可靠性和完全性定理.謂詞邏輯的不可判定性Hornformula的定義及其可滿足性算法..線性和立方SATsolver局限性。一階邏輯和高階邏輯在語法和表達能力差別？一階謂詞邏輯的項和公式是如何定義的，寫出他們的BNF范式并解釋之。解釋常用的線性時態(tài)邏輯公式的含義。解釋常用的分支時態(tài)邏輯公式的含義。程序的部分正確定性證明規(guī)則。簡單的程序部分正確性證明。了解ModelChecker和NuSMV。會用命題邏輯的自然演繹系統(tǒng)規(guī)則推導簡單的命題邏輯公式。會用謂詞邏輯邏的自然演繹系統(tǒng)規(guī)則推導簡單的謂詞邏輯公式。二命題邏輯語法的BNF范式及其解釋。P代表任意原子命題，：：=右邊的和每一次出現(xiàn)都表示任何已經(jīng)構造好的公式。命題邏輯的可靠性和完全性定理.設和是命題邏輯公式。若成立時，成立，則是可靠的。若成立時，成立，則是完全的。謂詞邏輯語法的BNF范式及其解釋。其中是1n元的謂詞符號，是F上的項，x是變量。在：：=的右邊，的每次出現(xiàn)都表示由上述規(guī)則構造出來的任意公式。線性時態(tài)邏輯的語法的的BNF范式及其解釋。其中P是取自某原子集atoms的任意命題原子。連接詞X,F,G,U,R和W稱為時態(tài)連接詞。分支時態(tài)邏輯的語法的的BNF范式及其解釋。此處p取遍原子公式的集合。每個CTL時態(tài)連接詞都是一對符號。對中的第一個是A或E。A是“沿所有路徑”（無一例外），E的含義是“沿至少（存在）一條路徑”（可能）。謂詞邏輯的可靠性和完全性定理.謂詞邏輯的不可判定性謂詞邏輯中的有效性問題是不可判定的：不存在對任意給定的，判定|=是否成立的程序。波斯特Hornformula的定義及其可滿足性算法.霍恩(Horn)公式是命題邏輯公式，如果它可以用下列語法作為H的實例產(chǎn)生：FunctionHORN()/*前置條件：是霍恩公式*//*后置條件：HORN()判定的可滿足性*/Beginfunction標記所有在中出現(xiàn)的（）；While中合取的所有都被標記時，do標記EndwhileIf被標記thenreturn“不是可滿足的”，Elsereturn“可滿足的”Endfunction線性和立方SATsolver局限性。無法判定形如的公式是否是可滿足的。一階邏輯和高階邏輯在語法和表達能力差別？一階邏輯指：命題邏輯和謂詞邏輯。高階邏輯指將量詞不僅應用于變量，而且應用于謂詞符號而產(chǎn)生的二階邏輯，如果對關系的關系取量詞，就可以得到三階邏輯，等等。階：只刻畫個體性質或關系的謂詞是一階謂詞，從而公式的形式看，一階謂詞只作用到個體變量或個體常量上。當對謂詞變量進行量化時，就進入了高階謂詞邏輯的范圍了。謂詞邏輯比命題邏輯有更強大的表達能為，它有謂詞，函數(shù)符號和量詞符號。但這是以犧牲有效性，可滿足性和可證明性的不可判定性為代價的。而謂詞不能表達可達性，高階邏輯可以表達，但高階邏輯在像完備性和緊密性這樣的典型結果可能很快就不再成立。而且一個樸素的高階邏輯在元邏輯級上可能是不相容的。一階謂詞邏輯的項和公式是如何定義的，寫出他們的BNF范式并解釋之。項定義如下：任何變量都是項；若F是零元函數(shù)，則c是項。若是項，且fF的元n>0，則是項。沒有其它形式的項。用backusnaur范式，可以寫：，其中x取遍F中的零元函數(shù)符號，f取遍F中的元n>0的符號。解釋常用的線性時態(tài)邏輯公式的含義。解釋常用的分支時態(tài)邏輯公式的含義。程序的部分正確定性證明規(guī)則。簡單的程序部分正確性證明。了解ModelChecker和NuSMV。NuSMV(有時簡稱SMV)提供描述一種用圖來描述的模型的語言，而且可以直接驗證基于這個模型的LTL(或CTL)公式的有效性。SMV的輸入是由描述模型的程序和一些規(guī)范(時態(tài)邏輯公式)組成。若