數(shù)理邏輯 復(fù)習(xí)提綱(11級(jí))

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