版權說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權,請進行舉報或認領
文檔簡介
人工智能原理
第3章
邏輯系統(tǒng)
1人工智能原理
第3章邏輯系統(tǒng)1
本章內(nèi)容
3.1命題邏輯和一階謂詞邏輯
3.2邏輯系統(tǒng)的語法和語義
3.3邏輯推理舉例
3.4邏輯智能體的推理策略
參考書目
附錄形式系統(tǒng)簡介第3章邏輯系統(tǒng)2 本章內(nèi)容
3.1命題邏輯和一階謂詞邏輯
3.2經(jīng)典數(shù)理邏輯AI研究內(nèi)容之一是推理,即研究怎樣使計算機獲得自動推理的能力數(shù)理邏輯用數(shù)學方法研究各種推理中的邏輯問題,以推理本身作為研究對象AI要使用邏輯推理,就必然涉及數(shù)理邏輯/數(shù)理邏輯的經(jīng)典部分—經(jīng)典的命題邏輯和一階謂詞邏輯,同時作為人工智能的知識表示方法和推理方法而存在;因此數(shù)理邏輯是人工智能的一個基礎第3章邏輯系統(tǒng)3經(jīng)典數(shù)理邏輯AI研究內(nèi)容之一是推理,即研究怎樣使計算機獲得自邏輯智能體基于知識的智能體的核心部件是知識庫,當這些知識以邏輯形式表示并進行相應的推理時,就是邏輯智能體知識表示:命題邏輯、一階謂詞邏輯推理(一階謂詞邏輯)—主要有3類推理算法:前向鏈接和演繹系統(tǒng)、反向鏈接和邏輯程序設計(本章)、歸結(jié)反演和定理證明系統(tǒng)(第4章)采用命題和謂詞演算進行推理的系統(tǒng)(如演繹系統(tǒng))是一種典型的邏輯智能體第3章邏輯系統(tǒng)4邏輯智能體基于知識的智能體的核心部件是知識庫,當這些知識以邏3.1命題邏輯和一階謂詞邏輯
命題、真值、原子公式、合式公式
謂詞、論域、個體
量詞、變量、函數(shù)
一階語言、一階語言的項第3章邏輯系統(tǒng)53.1命題邏輯和一階謂詞邏輯
命題、真值、原子公式、合式命題命題:描述客觀世界的可區(qū)分真假的陳述句,即判斷(經(jīng)典二值邏輯:非真即假)是命題的例子:2+2=4/二月份有30天/2002年哈爾濱有地震/人類能夠證明數(shù)論中所有論斷非真即假(有待時間)不是命題的例子:張三比李四聰明/公共汽車內(nèi)非常擁擠(各人認識不同)第3章邏輯系統(tǒng)6命題命題:描述客觀世界的可區(qū)分真假的陳述句,即判斷(經(jīng)典二命題變量與真值命題變量(變元):一個命題用符號表示,稱為命題符號當命題符號代表任一個命題時,即為命題變量真值:真或假–一個命題或命題變量具有真值真值連接詞(5個):否定/合取/析取/蘊涵/等價第3章邏輯系統(tǒng)7命題變量與真值命題變量(變元):一個命題用符號表示,稱為命題簡單命題與復合命題真值函數(shù):真值聯(lián)結(jié)詞可以視為一元或二元映射(真值函數(shù)),¬是從{T,F}到{T,F},其余是{T,F}2到{T,F}的映射/其函數(shù)定義由真值表確定簡單命題:一個被視為整體的、具有真或假的命題是簡單命題;復合命題:使用聯(lián)結(jié)詞將簡單命題聯(lián)結(jié)起來的命題是復合命題第3章邏輯系統(tǒng)8簡單命題與復合命題真值函數(shù):真值聯(lián)結(jié)詞可以視為一元或二元映射命題語言與原子公式命題邏輯:研究復合命題之間的推導關系命題語言:是命題邏輯使用的形式語言,是符號的集合,用Lp表示
/包括:命題符號、連接詞、左右括號原子公式:命題語言中的一個表達式是原子公式,當且僅當它是一個命題符號/原子公式也稱為文字(包括正文字和負文字)第3章邏輯系統(tǒng)9命題語言與原子公式命題邏輯:研究復合命題之間的推導關系第3章命題邏輯的合式公式合式公式(well-formedformula),簡稱公式,記作wff:一個表達式是一個公式,當且僅當它能通過有限次地使用下述步驟生成:(1)原子公式是公式;(2)如果A是公式,則(¬A)是公式;(3)如果A、B均為公式,則A*B是公式,其中*表示∧∨→≡中的任意一個/公式的形成規(guī)則/命題邏輯的主要研究對象是公式第3章邏輯系統(tǒng)10命題邏輯的合式公式合式公式(well-formedform謂詞從命題到一階謂詞:命題內(nèi)部邏輯結(jié)構(gòu)的分解對判斷的分解,把判斷中的具體內(nèi)容抽出,稱為個體;剩下的判斷即為謂詞謂詞可看作是從個體域或個體域的笛卡兒乘積到真值集合{T/F}的映射典型的推理例子:(1)凡人皆有死;(2)蘇格拉底是人;(3)蘇格拉底有死。(三段論式)M(x)D(x),M(s)├D(s)第3章邏輯系統(tǒng)11謂詞從命題到一階謂詞:命題內(nèi)部邏輯結(jié)構(gòu)的分解對判斷的分論域與個體論域和個體:在一階邏輯中,被研究對象構(gòu)成的非空集稱為論域;論域中的每個元素稱為個體論域例子:前面例子中的論域是“人”/所有的有理數(shù)都是實數(shù):其論域為有理數(shù)一階邏輯還研究個體之間的關系(或個體的性質(zhì))及作用于個體的函數(shù)論域/個體/個體間關系/作用于個體函數(shù)這4個成分構(gòu)成了一階邏輯的結(jié)構(gòu)第3章邏輯系統(tǒng)12論域與個體論域和個體:在一階邏輯中,被研究對象構(gòu)成的非空集稱謂詞謂詞(關系):一階形式語言中用于指稱論域中個體的性質(zhì)或者個體之間關系的形式符號(大寫字母表示)給定了論域,就確定了謂詞的真假值一元謂詞:個體的性質(zhì);二元謂詞(多元謂詞):個體的關系個體的位置—空位,具體化—構(gòu)成意義完整的語句空位的數(shù)目—謂詞的元數(shù)→幾元謂詞第3章邏輯系統(tǒng)13謂詞謂詞(關系):一階形式語言中用于指稱論域中個體的性質(zhì)或者量詞與變量變量(變元):表示論域內(nèi)的任意一個個體/常量(常元),表示確定的個體量詞與變量:量詞用來表示謂詞的判斷特性全稱量詞:對所有的xxP(x)存在量詞:存在xxP(x)約束變量:、中x的變量,量詞所管轄的公式如P(x)稱為量詞轄域自由變量:不在量詞轄域內(nèi)的變量為自由變量第3章邏輯系統(tǒng)14量詞與變量變量(變元):表示論域內(nèi)的任意一個個體/常量(約束變量和自由變量區(qū)別:自由變量可代入常量,約束變量不行,因為aP(a)無意義;約束變量可改名,自由變量不行帶有全稱變量x的命題表示為一階公式時,其表示形式為x(P(x)→…),帶有存在變量x的命題則表示形式為x(P(x)∧…)例子:所有有理數(shù)都是實數(shù)x(P(x)→R(x)),有些人身高超過2米x(M(x)∧G(x))上述使用方式不可改變,否則造成邏輯錯誤第3章邏輯系統(tǒng)15約束變量和自由變量區(qū)別:自由變量可代入常量,約束變量不行,因函數(shù)函數(shù):表示個體之間的運算,可作用于一個或數(shù)個個體(用小寫字母)給定一個或若干個體(對象),產(chǎn)生一個新的個體(對象)/函數(shù)的元數(shù)例子:x的父親father(張三)兩數(shù)之和仍是一個數(shù)add(e1,e2)第3章邏輯系統(tǒng)16函數(shù)函數(shù):表示個體之間的運算,可作用于一個或數(shù)個個體(用小寫函數(shù)與謂詞的區(qū)別謂詞和函數(shù)的區(qū)別:謂詞代表語句,結(jié)果是關系(具有真假值);函數(shù)代表關系運算,結(jié)果是一個新個體例子:謂詞SUM(e1,e2,e3)說明e1、e2、e3之間的關系是e1與e2的和是e3,函數(shù)add(e1,e2)說明e1與e2相加的結(jié)果仍是一個數(shù)第3章邏輯系統(tǒng)17函數(shù)與謂詞的區(qū)別謂詞和函數(shù)的區(qū)別:謂詞代表語句,結(jié)果是關系(一階語言(1)一階語言L:是一階邏輯使用的形式語言,可以和任何結(jié)構(gòu)(論域)沒有聯(lián)系,也可以與某個結(jié)構(gòu)有聯(lián)系與結(jié)構(gòu)沒有聯(lián)系的一階語言由8類符號組成:(1)無限序列的個體符號(個體常量)(2)無限序列的謂詞符號,有確定的元數(shù)n≥1有一個特殊的謂詞符號稱為相等符號(等式),記為=。L可含或不含=,如果含有,即稱為含=的一階邏輯第3章邏輯系統(tǒng)18一階語言(1)一階語言L:是一階邏輯使用的形式語言,可以和任一階語言(2)(3)無限序列的函數(shù)符號,有確定的元數(shù)m≥1(4)無限序列的自由變量:用u/v/w等表示自由變量(5)無限序列的約束變量:用x/y/z等表示約束變量(6)聯(lián)結(jié)詞:¬∧∨→≡(7)量詞:、(8)標點:左右括號、逗號(),第3章邏輯系統(tǒng)19一階語言(2)(3)無限序列的函數(shù)符號,有確定的元數(shù)m≥1第一階語言的項和公式L的項:一階語言中的一個符號是項t,當且僅當它能通過有限次使用下述步驟生成:
(1)個體常量、自由變量是項; (2)如果t1…tn是項,且f是n元函數(shù),則f(t1…tn)是項L的原子公式:一階語言中的一個表達式是一個原子公式,當且僅當它有如下2種形式:
(1)F(t1…tn),F(xiàn)是n元謂詞,t1…tn是項; (2)=(t1,t2)或t1=t2,t1、t2是項第3章邏輯系統(tǒng)20一階語言的項和公式L的項:一階語言中的一個符號是項t,當且僅一階語言的公式(1)L的公式:一階語言中的一個表達式是一個公式,當且僅當它能通過有限次使用下述步驟生成:(1)原子公式是公式;(2)如果A是公式,則(¬A)是公式;(3)如果A、B均為公式,則A*B是公式,其中*表示∧∨→≡中的任意一個(4)如果A(u)是公式,且x不在A(u)中出現(xiàn),則xA(x)、xA(x)都是公式第3章邏輯系統(tǒng)21一階語言的公式(1)L的公式:一階語言中的一個表達式是一個公一階語言的公式(2)一階謂詞公式的例子數(shù)學命題的表示:5只被1和5整除設Q(x,y)表示x被y整除,N(x)表示x是自然數(shù)
x(Q(5,x)→N(5)∨N(1))自然語言語句的表示:他不能在所有時刻欺騙所有人設F(x)表示“x是人”/G(x)“x是一個時刻”/H(x,y)“他能在y時刻欺騙x” ?xy(F(x)∧G(y)→H(x,y))或者 xy(?H(x,y)∧F(x)∧G(y))
第3章邏輯系統(tǒng)22一階語言的公式(2)一階謂詞公式的例子第3章邏輯系統(tǒng)223.2邏輯系統(tǒng)的語法和語義
邏輯系統(tǒng)的語法
邏輯系統(tǒng)的語義
語法和語義之間的關系第3章邏輯系統(tǒng)233.2邏輯系統(tǒng)的語法和語義
邏輯系統(tǒng)的語法
邏輯系統(tǒng)的語邏輯系統(tǒng)邏輯系統(tǒng)(亦稱形式系統(tǒng)FormalSystem)由5個部分組成:符號表—非空集合,即邏輯(形式)語言—如一階語言上全體符號的集合*的子集—項和變量*的子集—公式|公式和項的交集為空公式FORMULA上的子集—公理AXIOM公式上的n元關系集合—推理規(guī)則RULE、項TERM、FORMULA稱為FS的組成部分/AXIOM、RULE稱為FS的推演部分第3章邏輯系統(tǒng)24邏輯系統(tǒng)邏輯系統(tǒng)(亦稱形式系統(tǒng)FormalSystem)由語法和形式推演邏輯系統(tǒng)除符號表以外的部分構(gòu)成了邏輯系統(tǒng)的語法形式推演:定義了公式之間的形式可推演性關系,它涉及公式的語法結(jié)構(gòu),其正確性能夠機械地證明用記號├表示形式可推演關系,讀作“推出”用├A表示A是由形式可推演的(或形式可證明的),其中是前提,A是結(jié)論第3章邏輯系統(tǒng)25語法和形式推演邏輯系統(tǒng)除符號表以外的部分構(gòu)成了邏輯系統(tǒng)的語法推演規(guī)則舉例形式推演由形式推演規(guī)則定義,舉例如下:自反 A├A (Ref)傳遞 if├‘├Athen├A ()¬消去(反證律) if,¬A├B&,¬A├¬B then├A (¬–)公式變換 A→BAB第3章邏輯系統(tǒng)26推演規(guī)則舉例形式推演由形式推演規(guī)則定義,舉例如下:第3章邏形式可推演性形式可推演性:在命題/一階邏輯系統(tǒng)中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應用相應邏輯的形式推演規(guī)則生成即├A成立,當且僅當存在有限序列使得1├A1,2├A2,…,n├An
中的每一項均由某個形式推導規(guī)則生成,且n├An
就是├A即n=,An=A建立在上述形式推演規(guī)則基礎上的形式推演系統(tǒng)稱為自然推演(演繹)系統(tǒng)第3章邏輯系統(tǒng)27形式可推演性形式可推演性:在命題/一階邏輯系統(tǒng)中,A是由可邏輯系統(tǒng)的語義語義即對形式語言進行解釋研究可推導性即形式推演(├)時不考慮作為前提和結(jié)論的命題的內(nèi)容,只考慮命題真假并由此確定前提的真是否蘊涵結(jié)論的真,即前提和結(jié)論之間是否有可推導關系(語法)研究形式系統(tǒng)的語義時,對邏輯系統(tǒng)賦予研究對象的集合即論域;用論域中的個體對象、對象之上的運算(函數(shù))、對象之間的關系(謂詞)去解釋邏輯系統(tǒng)中的符號,稱作指稱denote指稱語義學賦予形式系統(tǒng)的論域及解釋稱為形式系統(tǒng)的語義結(jié)構(gòu),簡稱結(jié)構(gòu)(structure)第3章邏輯系統(tǒng)28邏輯系統(tǒng)的語義語義即對形式語言進行解釋第3章邏輯系統(tǒng)28命題邏輯的語義與可滿足性研究命題邏輯的語義,即研究公式(公式集)的真假賦值問題真假賦值:真假賦值是以所有命題符號的集合為定義域、以真假值{1,0}為值域的函數(shù)。真假賦值v給公式A指派的值記作Av可滿足性:是可滿足的,當且僅當有真假賦值v,使得v=1。此時稱v滿足。第3章邏輯系統(tǒng)29命題邏輯的語義與可滿足性研究命題邏輯的語義,即研究公式(公式可滿足性的可滿足性蘊涵了中所有公式的可滿足性,但反過來不成立。因為這要求同一個真假賦值滿足所有的公式(并非所有可滿足的公式使用同一個賦值)重言式和矛盾式A是重言式(永真式),當且僅當對于任意的真假賦值v,Av=1A是矛盾式(永假式),當且僅當對于任意的真假賦值v,Av=0第3章邏輯系統(tǒng)30可滿足性的可滿足性蘊涵了中所有公式的可滿足性,但反過來不真假判斷與邏輯推論一個命題公式是重言式或者是矛盾式或者兩者都不是,需要進行判定。判定方法可通過構(gòu)造真假值表方法或采用樹形分支的方法來判定可推導關系:研究前提的真是否蘊涵結(jié)論的真,引入語義以后對公式進行真假賦值;如果對任意的真假賦值,都有上述關系,則說明前提和結(jié)論之間存在一種邏輯推論關系(或稱邏輯蘊涵)第3章邏輯系統(tǒng)31真假判斷與邏輯推論一個命題公式是重言式或者是矛盾式或者兩者都命題邏輯的邏輯推論邏輯推論:設、A分別是命題邏輯中的公式集合和公式,A是的邏輯推論,記為A,當且僅當對于任意真假賦值v,v=1蘊涵Av=1。|=可讀作“邏輯地蘊涵”,|=是前提和結(jié)論A之間的關系邏輯推論的證明要證明|=A時,即要證明對于任何真假賦值v,如果v=1則Av=1(通常使用反證法)第3章邏輯系統(tǒng)32命題邏輯的邏輯推論邏輯推論:設、A分別是命題邏輯中的公式集一階語言的語義一階語言的語義:一階語言的解釋包括一個論域和一個函數(shù)函數(shù)把一階語言中的個體符號映射到論域中的個體n元關系符號(即謂詞)映射到論域上的n元關系m元函數(shù)符號映射到論域上的m元全函數(shù)以上組成了該論域中對一階語言的解釋第3章邏輯系統(tǒng)33一階語言的語義一階語言的語義:一階語言的解釋包括一個論域和一一階語言的賦值賦值:一階語言L的賦值v包括一個論域D和一個函數(shù)(記作v)L中所有個體符號a為定義域,其賦值v(a)或av
關系符號F的賦值v(F)或Fv
函數(shù)符號f的賦值v(f)或fv自由變量符號u的賦值v(u)或uv則有
(1)av,uv∈D (2)FvDn (3)fv:Dm→D第3章邏輯系統(tǒng)34一階語言的賦值賦值:一階語言L的賦值v包括一個論域D和一個函一階邏輯的邏輯推論公式的真假值:一階語言的公式在以D為論域的賦值之下,其真假值可以遞歸定義一階邏輯的邏輯推論:與命題邏輯相同,只是這里不使用真假賦值,而用賦值邏輯推論:設、A分別是一階語言的公式集和公式,A是的邏輯推論,記作|=A,當且僅當對于任何賦值v,v=1蘊涵Av=1一階邏輯的邏輯推論證明方法類似于命題邏輯,常用反證法。但對于否證邏輯推論,則需要構(gòu)造賦值所需的論域。確定論域時,關鍵在于論域的大小第3章邏輯系統(tǒng)35一階邏輯的邏輯推論公式的真假值:一階語言的公式在以D為論域的邏輯系統(tǒng)的整體特征在經(jīng)典邏輯的形式系統(tǒng)中,形式推演是語法概念,邏輯推論是語義概念形式系統(tǒng)的整體特征:是在形式系統(tǒng)引入語義以后,研究對于任何一階語言的公式集和公式A在何種賦值的條件下,其結(jié)果是否為真—即研究形式推演與邏輯推論之間的關系賦值的條件:給定某個賦值—可滿足性給定任意賦值—有效性第3章邏輯系統(tǒng)36邏輯系統(tǒng)的整體特征在經(jīng)典邏輯的形式系統(tǒng)中,形式推演是語法概念可靠性定理與完備性定理對于任何一階語言的公式集和公式A,├A|=A表示:凡是形式可推演性所反映的前提和結(jié)論之間的關系,在非形式的推理中都是成立的,即形式可推演性對于反映非形式的推理是可靠的,此即可靠性定理(或者稱合理性)|=A├
A表示:凡是在非形式推理中成立的前提和結(jié)論之間的關系,形式可推演性都是能夠反映的,即形式可推演性在反映非形式推理時沒有遺漏,此即完備性定理第3章邏輯系統(tǒng)37可靠性定理與完備性定理對于任何一階語言的公式集和公式A,第可滿足性與有效性(1)不加證明地給出有關定義和定理可滿足性—一階邏輯公式集合是可滿足的,當且僅當有(以某個不空集為論域)賦值v,使得v=1/當v=1時,稱v滿足反過來,不可滿足性就是對任意論域上的任意賦值都有v=0第3章邏輯系統(tǒng)38可滿足性與有效性(1)不加證明地給出有關定義和定理第3章邏可滿足性與有效性(2)有效性:一階邏輯公式A是有效的,當且僅當對于(以任何不空集為論域)任何賦值v,Av=1/有效性也稱為普遍有效性論域中的可滿足性、有效性:(1)在D中是可滿足的,當且僅當有以D為論域的賦值v,使得v=1(2)A在D中是有效的,當且僅當對于任何以D為論域的賦值v,Av=1第3章邏輯系統(tǒng)39可滿足性與有效性(2)有效性:一階邏輯公式A是有效的,當且僅可滿足性與有效性(3)(關于命題的)定理:(1)A是可滿足的,當且僅當?A是不有效的;(2)A是有效的,當且僅當?A是不可滿足的。(關于一階的)定理:(1)A(u1,…,un)是可滿足的,當且僅當x1...xnA(x1,…,xn)是可滿足的(2)A(u1,…,un)是有效的,當且僅當x1...xnA(x1,…,xn)是有效的第3章邏輯系統(tǒng)40可滿足性與有效性(3)(關于命題的)定理:(1)A是可滿足可靠性定理可靠性定理[1]:設Form(L),A∈Form(L)(也包括了命題語言Lp) (1)如果├A,則|=A; (2)如果├A,則|=A(即所有形式可推演的都是有效的)協(xié)調(diào)性(無矛盾性):Form(L)是協(xié)調(diào)的,當且僅當不存在A∈Form(L),使得├A且├?A可靠性定理[2]:設Form(L),A∈Form(L) (1)如果是可滿足的,則是協(xié)調(diào)的; (2)如果A是可滿足的,則A是協(xié)調(diào)的。([1][2]等價)第3章邏輯系統(tǒng)41可靠性定理可靠性定理[1]:設Form(L),A∈For完備性定理命題邏輯和一階邏輯的完備性定理[1]:設Form(L),A∈Form(L)(含Lp) (1)如果是協(xié)調(diào)的,則是可滿足的; (2)如果A是協(xié)調(diào)的,則A是可滿足的。定理[2]:設Form(L),A∈Form(L) (1)如果|=A,則├A; (2)如果|=A,則├A(所有有效公式都是形式可證明公式)。如果對論域限定以后,可得更精確的陳述第3章邏輯系統(tǒng)42完備性定理命題邏輯和一階邏輯的完備性第3章邏輯系統(tǒng)423.3邏輯推理舉例
wumpus世界
命題邏輯推理模式
基于電路的智能體第3章邏輯系統(tǒng)433.3邏輯推理舉例
wumpus世界
命題邏輯推理模式wumpus世界(1)Wumpus是一個早期電腦游戲中的怪物Agent感知:陷阱旁邊有微風breeze怪獸旁邊有惡臭stench金子閃閃發(fā)光glitter感覺墻的反彈陷阱和怪物的位置隨機生成第3章邏輯系統(tǒng)stenchBreezePitWumpus(Monster)BreezeStenchGoldPitBreezestenchBreezeAgentBreezePitBreeze44wumpus世界(1)Wumpus是一個早期電腦游戲中的怪物wumpus世界(2)Wumpus世界搜索圖示—感知用5元組表示
[感知wumpus,感知微風,感知金光,感知墻,感知wumpus被殺死] A=Agent B=Breeze G=Glitter,Gold OK=safesquare P=Pit S=Stench V=visited W=wumpus N=None1,42,43,44,41,32,33,34,31,2OK2,23,24,21,1
AOK2,1OK3,14,1第3章邏輯系統(tǒng)1,42,43,44,41,32,33,34,31,2OK2,2P?3,24,21,1VOK2,1ABOK3,1P?4,1(a)[N,N,N,N,N] (b)[N,B,N,N,N]45wumpus世界(2)Wumpus世界搜索圖示—感知用5元組wumpus世界(3)1,42,43,44,41,3W!2,33,34,31,2ASOK2,2OK3,24,21,1VOK2,1BVOK3,1P!4,1第3章邏輯系統(tǒng)1,42,4P?3,44,41,3W!2,3ABSG3,3P?4,31,2S
VOK2,2VOK3,24,21,1VOK2,1BVOK3,1P!4,1A=Agent B=Breeze G=Glitter,Gold OK=safesquareP=Pit S=Stench V=visited W=wumpus N=None(c)[S,N,N,N,N] (d)[S,B,G,N,N]46wumpus世界(3)1,42,43,44,41,32,33wumpus世界中的命題和推理規(guī)則只考慮陷阱的情況Pi,j=T—[i,j]中有陷阱,記為Pi,jBi,j=T—[i,j]中有微風,記為Bi,j規(guī)則如下:R1 P1,1R2 B1,1P1,2P2,1R3 B2,1P1,1P2,2P3,1R4 B1,1R5 B2,1第3章邏輯系統(tǒng)47wumpus世界中的命題和推理規(guī)則只考慮陷阱的情況第3章邏命題邏輯推理模式分離規(guī)則與消去邏輯等價(雙向蘊涵消去)第3章邏輯系統(tǒng)48命題邏輯推理模式分離規(guī)則第3章邏輯系統(tǒng)48wumpus世界的推理例子用R1~R5規(guī)則和推理模式證明:[1,2]和[2,1]中沒有陷阱,即P1,2和P2,1證明:從R2開始R6 (B1,1(P1,2∨P2,1))∧((P1,2∨P2,1)B1,1) R2雙向蘊涵消去R7 (P1,2∨P2,1)B1,1 R6與消去R8 ?B1,1?(P1,2∨P2,1) 逆否命題邏輯等價R9 ?(P1,2∨P2,1) R4/R8分離規(guī)則R10(結(jié)果) ?P1,2∧?P2,1 迪摩根定律第3章邏輯系統(tǒng)49wumpus世界的推理例子用R1~R5規(guī)則和推理模式證明:[基于電路的智能體基于電路的智能體的目的:把對現(xiàn)狀的感知變?yōu)橹悄荏w的行動感知=input→判斷/行動判斷:尖叫→怪獸wumpus將死亡行動:金光→抓起金子/行動控制=寄存器第3章邏輯系統(tǒng)grabglitterAlive延遲Scream
50基于電路的智能體基于電路的智能體的目的:把對現(xiàn)狀的感知變?yōu)橹莣umpus世界中智能體的判斷(1)位置判斷:在L1,1—分為3種情況:一直留在[1,1],從[1,2]走到[1,1],從[2,1]走到[1,1]使用位置寄存器/狀態(tài)寄存器第3章邏輯系統(tǒng)L1,2L2,1facing-leftfacing-down∧∧?∧∨∨L1,1forwardbump51wumpus世界中智能體的判斷(1)位置判斷:在L1,1—分wumpus世界中智能體的判斷(2)上述電路圖表示為邏輯表達式
第3章邏輯系統(tǒng)前述電路的邏輯表達式判斷wumpus是否活著發(fā)現(xiàn)金子后的行動但因為沒有變量,不能表示更一般的情況,如不同位置用同一個邏輯式52wumpus世界中智能體的判斷(2)上述電路圖表示為邏輯表達3.4邏輯智能體的推理策略
邏輯智能體構(gòu)造
Horn子句
置換與合一
前向鏈接算法/后向鏈接算法第3章邏輯系統(tǒng)533.4邏輯智能體的推理策略
邏輯智能體構(gòu)造
Horn子句邏輯智能體的構(gòu)造(1)以一階謂詞演算為核心的邏輯系統(tǒng)是典型的邏輯智能體系統(tǒng)的基礎是一階語言,由此構(gòu)造知識庫/一般構(gòu)造知識庫(知識工程)的過程包括:確定任務收集相關知識確定謂詞、函數(shù)和常量詞匯表第3章邏輯系統(tǒng)54邏輯智能體的構(gòu)造(1)以一階謂詞演算為核心的邏輯系統(tǒng)是典型的邏輯智能體的構(gòu)造(2)對領域(論域)的通用知識進行編碼對特定問題實例的描述進行編碼查詢提交、推理、給出答案調(diào)試知識庫如果采用一階語言的特殊形式—確定子句Horn子句,可獲得高效推理第3章邏輯系統(tǒng)55邏輯智能體的構(gòu)造(2)對領域(論域)的通用知識進行編碼第3章Horn子句Horn子句(HornClause):是一類至多只有一個正文字的子句(子句=文字的析取式)例子:?A∨?B∨C(注意:這是一般公式AB→C的變形)Horn子句稱為確定子句,其中正文字稱為子句的頭,負文字構(gòu)成子句的體第3章邏輯系統(tǒng)56Horn子句Horn子句(HornClause):是一類至Horn子句的性質(zhì)只有一個正文字的約束具有重要意義:每個Horn子句實際上都是一個蘊涵式的變形,實際知識庫中常常使用這樣易懂的形式/沒有正文字的Horn子句可以寫成結(jié)論為FALSE的蘊涵式Horn子句的推理可以使用前向鏈接和后向鏈接算法用Horn子句判定蘊涵所需時間與數(shù)據(jù)庫成線性關系最重要的是最后一個性質(zhì)第3章邏輯系統(tǒng)57Horn子句的性質(zhì)只有一個正文字的約束具有重要意義:第3章推理策略簡要介紹2種推理算法—簡單的前向鏈接算法和簡單的后向鏈接算法,結(jié)合一個例子說明算法的應用一階推理規(guī)則—一般化分離規(guī)則(GeneralizedModusPonens)對于原子語句pi,pi’,q,存在置換,使得(pi)=(pi’),對所有i都成立,則第3章邏輯系統(tǒng)58推理策略簡要介紹2種推理算法—簡單的前向鏈接算法和簡單的后向置換與合一置換(或代換):設x1~xn是n個變量,且各不相同,t1~tn是n個項(常量、變量、函數(shù)),ti≠xi,則有限序列{t1/x1,t2/x2…tn/xn}稱為一個置換置換乘積(合成):設和是2個置換,則先后作用于公式或項,稱為置換乘積,用表示。通過相關的置換,使不同的一階公式成為一樣的,這個過程稱為合一第3章邏輯系統(tǒng)59置換與合一置換(或代換):設x1~xn是n個變量,且各不相同合一置換合一置換:設有一組謂詞公式{E1~Ek}和置換,使E1=E2=…=Ek,則稱為合一置換,E1~Ek稱為可合一的/合一置換也叫通代最一般合一置換(最廣通代):如果和都是公式組{E1~Ek}的合一置換,且有置換存在,使得=,則稱為公式組{E1~Ek}的最一般合一置換,記為mgu(mostgeneralunification)第3章邏輯系統(tǒng)60合一置換合一置換:設有一組謂詞公式{E1~Ek}和置換,使置換與合一的例子有子句xKing(x)∧Greedy(x)→Evil(x)King(John)Greedy(John)則做置換={x/John},用一般化分離規(guī)則可得:q=Evil(John)第3章邏輯系統(tǒng)61置換與合一的例子有子句第3章邏輯系統(tǒng)61合一結(jié)果對于合一UNIFY,合一的結(jié)果是一個置換,如:UNIFY(Know(John,x),Know(John,Jane))={x/Jane}UNIFY(Know(John,x),Know(y,Mary))={x/Mary,y/John}但是UNIFY(K(John,x),K(x,Jane))=FAIL,原因是x不能同時選取2個值詳細的合一算法將在第6章介紹第3章邏輯系統(tǒng)62合一結(jié)果對于合一UNIFY,合一的結(jié)果是一個置換,如:第用于邏輯推理的例子問題描述:美國法律規(guī)定:美國人(American)賣武器(weapon)給敵對國家(hostile)是犯罪的(criminal).美國的敵國Nono有一些導彈(missile),所有這些導彈是West上校賣給他們的,而West上校是一個美國人證明:West是犯罪的第3章邏輯系統(tǒng)63用于邏輯推理的例子問題描述:第3章邏輯系統(tǒng)63問題用一階子句表示(1)用確定子句表示上述內(nèi)容美國人賣武器給敵對國家是犯罪的American(x)∧Weapon(y)∧Sell(x,y,z)∧Hostile(z)→Criminal(x) [1]Nono有一些導彈xOwn(Nono,x)∧Missile(x) 消去其中的存在量詞,引入新常量,得到2個原子公式(正文字)Own(Nono,M1) [4]Missile(M1) [5]第3章邏輯系統(tǒng)64問題用一階子句表示(1)用確定子句表示上述內(nèi)容第3章邏輯系問題用一階子句表示(2)所有該國導彈都是West上校出售的Missile(y)∧Own(Nono,y)→Sell(West,y,Nono)[2]導彈是武器Missile(y)→Weapon(y) [3]其它陳述:美國人West American(West) [6]敵國Nono Hostile(Nono) [7]上述描述放入知識庫:[1]~[3]為確定子句(上述原始形式均可以化為原子的析取且只有一個正文字),[4]~[7]為正文字第3章邏輯系統(tǒng)65問題用一階子句表示(2)所有該國導彈都是West上校出售的第前向鏈接算法的說明(1)前向鏈接算法的推理過程:從已知事實(知識庫中的原子公式)開始,依次對知識庫中的規(guī)則(以確定子句的形式出現(xiàn))進行置換,檢查規(guī)則前提部分的文字是否全部與知識庫中的事實相匹配如果是匹配的,則把該條規(guī)則已經(jīng)做過置換的結(jié)論部分添加到知識庫中,如果這個結(jié)論和查詢(既需要推導出的結(jié)論)一致,則推理結(jié)束,獲得證明第3章邏輯系統(tǒng)66前向鏈接算法的說明(1)前向鏈接算法的推理過程:第3章邏輯前向鏈接算法的說明(2)重復上述過程,直到獲得證明;或者再沒有新的事實(推出的結(jié)論)加入,則此時推理以證明失敗結(jié)束約束:要求每次加入知識庫的結(jié)論都是全新的,而不是已知事實的重命名(即謂詞相同只是變量名不同)第3章邏輯系統(tǒng)67前向鏈接算法的說明(2)重復上述過程,直到獲得證明;或者再沒簡單的前向鏈接算法FunctionFC(KB,α)ReturnasubstitutionorFALSE Inputs:KB,asetoffirst-orderdefiniteclauses/,thequery=anatom localvariables:new,thenewrulesinferredoneachiteration repeatuntilnewisempty
new←{} foreachruler(intheformofdefineclause)inKBdo
foreachsuchthat(p1∧…∧pn)=(p1’∧…∧pn’) get(q)=q’ ifq’isnew(satisfiedtheconstraint) thendoaddq’tonew ←UNIFY(q’,)
Ifisnotfailthenreturn addnewtoKB returnfalse第3章邏輯系統(tǒng)68簡單的前向鏈接算法FunctionFC(KB,α)Ret前向鏈接算法例子(1)第3章邏輯系統(tǒng)使用前向鏈接算法對前面的例子進行推理用知識庫中的事實(即[4]~[7])依次對知識庫中的各個子句進行置換操作并用推理規(guī)則獲得新的文字第一次循環(huán)體執(zhí)行:子句[1]前提部分未獲滿足(為什么?)子句[2]—使用置換{x/M1},則可得 Sell(West,M1,Nono) [8]子句[3]—使用置換{x/M1},則可得Weapon(M1) [9]69前向鏈接算法例子(1)第3章邏輯系統(tǒng)使用前向鏈接算法對前面前向鏈接算法例子(2)第3章邏輯系統(tǒng)此時new中為[8][9],為原知識庫所未有,將它們添加到知識庫中第二次循環(huán)體執(zhí)行:再次循環(huán)時new首先清空子句[1]—置換{x/West,y/M1,z/Nono} 得到Criminal(West) [10]添加到new中,與查詢進行合一測試,一致則返回/算法結(jié)束70前向鏈接算法例子(2)第3章邏輯系統(tǒng)此時new中為[8][前向鏈接生成的證明樹第3章邏輯系統(tǒng)Criminal(West)Weapon(M1)Sells(West,M1,Nono)Hostile(Nono)American(West)Missile(M1)Owns(Nono,M1)Enemy(Nono,America)71前向鏈接生成的證明樹第3章邏輯系統(tǒng)Criminal(Wes反向鏈接算法的說明(1)原始查詢(既要證明的結(jié)論)以目標列表的形式出現(xiàn),開始時列表中只有一個元素列表的操作相當于棧,是一個遞歸過程(如下)即深度優(yōu)先的搜索過程推理過程是從結(jié)論(子句的頭)開始,找到匹配的頭就擴展這個頭所在的規(guī)則體;擴展部分又作為頭繼續(xù)擴展,直到全部原子均與事實相匹配比較:正向=事實結(jié)論/反向=結(jié)論事實第3章邏輯系統(tǒng)72反向鏈接算法的說明(1)原始查詢(既要證明的結(jié)論)以目標列表反向鏈接算法的說明(2)算法的推理過程是:選取棧當中的第一個目標,在知識庫中尋找子句的頭(即結(jié)論部分)能與目標合一的每個子句每個這樣的子句創(chuàng)建了一個遞歸調(diào)用過程,在這個遞歸調(diào)用過程中子句的前提(子句的體)被加入到目標棧當中當棧中所有目標都得到匹配,則當前的證明分支是成功的注意:事實是指有頭沒有體的子句(正文字)第3章邏輯系統(tǒng)73反向鏈接算法的說明(2)算法的推理過程是:第3章邏輯系統(tǒng)7反向鏈接算法的說明(3)在算法中answers作為存放置換的數(shù)據(jù)結(jié)構(gòu),返回一系列置換操作,這些操作說明了反向鏈接算法獲取證明的過程在算法中包括了置換的合成’(或者寫為Compose(’,)),其效果就是依次進行每個置換第3章邏輯系統(tǒng)74反向鏈接算法的說明(3)在算法中answers作為存放置換的反向鏈接算法的說明(4)第一次應用算法,對于待證明的目標來說,本身就是一個正文字,此時要用這個文字中的常量對合適的規(guī)則(子句的頭與該文字匹配)進行置換這個置換通過遞歸調(diào)用帶入下一次置換,就得到了合成置換在本例中有:初始{x/West} 遞歸{x/West,y/M1} 遞歸{x/West,y/M1,z/Nono}第3章邏輯系統(tǒng)75反向鏈接算法的說明(4)第一次應用算法,對于待證明的目標來說簡單的反向鏈接算法FunctionBC(KB,goals,)returnsasetofsubstitutions
Inputs:KB,goals=alistofconjunctsformingaquery(alreadyapplied),=thecurrentsubstitution(initial={})
localvariables:answers=asetofsubstitutions(initial={})
ifgoalsisemptythenreturn{} q’=(FIRST(goals)) (初始為空,遞歸以后不空) foreachruler(intheformofdefineclause)inKBand ’=UNIFY(q,q’)succeeds new_goal={p1’,…,pn’}asREST(goals) answers=BC(KB,new_goal,’))∪answers returnanswers第3章邏輯系統(tǒng)76簡單的反向鏈接算法FunctionBC(KB,goals反向鏈接算法例子(1)反向鏈接算法推理過程目標Criminal(West)分解為公式[1]前提部分的4個文字,即American(West),Weapon(y),Sell(West,y,z),Hostile(z)—置換={x/West}American(West)和事實相匹配需要遞歸匹配:Weapon(y),Sell(West,y,z),Hostile(z)Weapon(y)遞歸調(diào)用前={x/West},進入第一次遞歸產(chǎn)生Missile(M1),此時置換{y/M1}匹配,遞歸返回復合={x/West,y/M1}第3章邏輯系統(tǒng)77反向鏈接算法例子(1)反向鏈接算法推理過程第3章邏輯系統(tǒng)7反向鏈接算法例子(2)再次遞歸調(diào)用Sell(West,M1,z)—得到置換={z/Nono},遞歸返回復合置換{x/West,y/M1,z/Nono}在置換過程中每個變量只能置換一個常量作為約束,減少置換的不定性此時子目標全部匹配,再無新的子目標生成,返回置換集合結(jié)束第3章邏輯系統(tǒng)78反向鏈接算法例子(2)再次遞歸調(diào)用Sell(West,M1反向鏈接生成的證明樹第3章邏輯系統(tǒng)Criminal(West)American(West)Weapon(y)Sells(West,M1,z)Hostile(Nono)Missile(y)Missile(M1)Owns(Nono,M1)Enemy(Nono,Amerca){}z/Nono{}{}{}{y/M1}79反向鏈接生成的證明樹第3章邏輯系統(tǒng)Criminal(Wes正向鏈接和反向鏈接前向鏈接算法特點:數(shù)據(jù)驅(qū)動/是可靠的和完備的后向鏈接算法特點:目標驅(qū)動/是可靠的但不是完備的(書中p220/p224)可以從“是否能找到問題的解”角度考慮不完備性后向鏈接算法根據(jù)目標來進行相關事實的匹配,對于大規(guī)模的知識庫來說有助于減小搜索空間第3章邏輯系統(tǒng)80正向鏈接和反向鏈接前向鏈接算法特點:數(shù)據(jù)驅(qū)動/是可靠的和參考書目StuartRussell/PeterNorvig:AIMA第7章/第8章/第9章陸汝鈐編著:人工智能(上冊)第1章陸鐘萬,面向計算機科學的數(shù)理邏輯,科學出版社,1998年1月第1版朱梧[木賈]、肖奚安,數(shù)理邏輯引論,南京大學出版社,1995年5月第1版王元元,計算機科學中的邏輯學,科學出版社,1989年9月第1版第3章邏輯系統(tǒng)81參考書目StuartRussell/PeterNor附錄形式系統(tǒng)簡介
F1形式系統(tǒng)和形式推演
F2形式系統(tǒng)的語義
F3形式系統(tǒng)的整體特征第3章邏輯系統(tǒng)82附錄形式系統(tǒng)簡介
F1形式系統(tǒng)和形式推演
F2形式系F1形式系統(tǒng)定義和形式推演第3章邏輯系統(tǒng)83F1形式系統(tǒng)定義和形式推演第3章邏輯系統(tǒng)83形式系統(tǒng)定義(1)邏輯的形式系統(tǒng)的定義–一個形式系統(tǒng)FormalSystem由5個部分組成:(1)符號表,非空集合,即形式語言(如Lp和L);(2)上全體符號的集合*的一個子集TERM,其元素稱為FS的項;TERM有子集VARIABLE,其元素稱為變量;(3)*的一個子集FORMULA,其元素稱為FS的公式;FORMULA有子集ATOM,其元素稱為原子公式;TERMFORMULA=;第3章邏輯系統(tǒng)84形式系統(tǒng)定義(1)邏輯的形式系統(tǒng)的定義–一個形式系統(tǒng)Fo形式系統(tǒng)定義(2)(4)FORMULA的一個子集AXIOM,其元素稱為FS的公理;(5)FORMULA上的n元關系集合RULE,其元素稱為FS的推理規(guī)則。其中、TERM、FORMULA稱為FS的組成部分,AXIOM、RULE稱為FS的推演部分公理推演系統(tǒng)包括AXIOM,而自然推演系統(tǒng)只包括推理規(guī)則第3章邏輯系統(tǒng)85形式系統(tǒng)定義(2)(4)FORMULA的一個子集AXIOM,對象語言和元語言(1)對象語言和元語言:作為被研究對象的語言稱為對象語言,用以研究對象語言的語言稱為元語言例子:用漢語研究英語語法,則英語是對象語言,漢語是元語言數(shù)理邏輯中的形式系統(tǒng)各有其自身的形式語言如Lp和L,這些是被研究的對象,因而是對象語言;但為了研究這些形式系統(tǒng),又必須使用某種語言,那么這種語言便是元語言第3章邏輯系統(tǒng)86對象語言和元語言(1)對象語言和元語言:作為被研究對象的語言對象語言和元語言(2)如:“鳥正在飛翔”—描述—對象語言;“命題‘鳥正在飛翔’真”—對上句的評論—元語言。形式系統(tǒng)的對象語言,其中的符號既是對客觀對象的抽象,用于研究客觀對象;同時又是一種符號客體,是被研究的對象第3章邏輯系統(tǒng)87對象語言和元語言(2)如:“鳥正在飛翔”—描述—對象語言;“對象語言和元語言(3)形式系統(tǒng)的元語言包括:對形式系統(tǒng)中組成成分的稱謂—項、公式、公理等邏輯術語—如果-那么、當且僅當、存在、所有等對形式系統(tǒng)性質(zhì)(整體特征)的描述—如一致性、完備性、可判定性等,該部分最重要元語言中使用的符號:自然語言(如漢語)和一些被引進的符號,如:├、|=等未經(jīng)解釋的形式語言可以沒有含義,但元語言必須有其具體含義。第3章邏輯系統(tǒng)88對象語言和元語言(3)形式系統(tǒng)的元語言包括:第3章邏輯系統(tǒng)元理論元理論是關于形式系統(tǒng)的理論,包括三部分內(nèi)容:關于形式系統(tǒng)語法(syntax)的研究,不涉及具體意義的符號體系,研究符號串的推演,即形式推演;關于形式系統(tǒng)語義(semantics)的研究,研究形式系統(tǒng)在被作出各種解釋時的性質(zhì);關于形式系統(tǒng)語法和語義關系的研究,特別是形式系統(tǒng)的性質(zhì),如:合理性、完備性等。第3章邏輯系統(tǒng)89元理論元理論是關于形式系統(tǒng)的理論,包括三部分內(nèi)容:第3章邏形式推演形式推演:定義了公式之間的形式可推演性關系,它涉及公式的語法結(jié)構(gòu),其正確性能夠機械地證明用記號├表示形式可推演關系,讀作“推出”用├A表示A是由形式可推演的(或形式可證明的),其中是前提,A是結(jié)論記號├不是形式語言中的符號,├A也不是形式語言中的公式,而是元語言中的命題第3章邏輯系統(tǒng)90形式推演形式推演:定義了公式之間的形式可推演性關系,它涉及公常用推演規(guī)則(1)形式推演由形式推演的規(guī)則定義命題邏輯中有一些常用的推演規(guī)則(規(guī)則模式)肯定前提 ifA∈then├A (∈)增加前提 if├Athen,‘├A(+)自反 A├A (Ref)傳遞 if├‘├Athen├A()第3章邏輯系統(tǒng)91常用推演規(guī)則(1)形式推演由形式推演的規(guī)則定義第3章邏輯系常用推演規(guī)則(2)¬消去(反證律) if,¬A├B&,¬A├¬B then├A (¬-)¬引入(歸謬律) if,A├B&,A├¬B then├¬A (¬+)→消去 if├A→B,├A then├B (→-)→引入if,A├B then├A→B (→+)第3章邏輯系統(tǒng)92常用推演規(guī)則(2)¬消去(反證律) 第3章邏輯系統(tǒng)92常用推演規(guī)則(3)∧消去if├A∧Bthen├A,├B (∧-)∧引入 if├A,├Bthen├A∧B (∧+)∨消去if,A├C&,B├Cthen,A∨B├C(∨-)∨引入if├A
then├A∨B,├B∨A (∨+)第3章邏輯系統(tǒng)93常用推演規(guī)則(3)∧消去第3章邏輯系統(tǒng)93常用推演規(guī)則(2)≡消去if├A≡B,├Athen├Bif├A≡B,├Bthen├A (≡-)≡引入if,A├B&,B├A then├A≡B (≡+)通過連接詞的增減或變形,實現(xiàn)公式的變換常用A→BAB第3章邏輯系統(tǒng)94常用推演規(guī)則(2)≡消去第3章邏輯系統(tǒng)94形式可推演性(1)(命題邏輯)形式可推演性:在命題邏輯中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應用命題邏輯的形式推演規(guī)則生成即├A成立,當且僅當存在有限序列使得1├A1,2├A2,…,n├An
中的每一項均由某個形式推導規(guī)則生成,且n├An
就是├A即n=,An=A第3章邏輯系統(tǒng)95形式可推演性(1)(命題邏輯)形式可推演性:在命題邏輯中,A形式可推演性(2)用
A表示├A不成立用A|-|B表示左右兩邊的公式可以互相推出,稱其為語法等值公式或等值公式建立在上述形式推演規(guī)則基礎上的形式推演系統(tǒng)稱為自然推演(演繹)系統(tǒng)第3章邏輯系統(tǒng)96形式可推演性(2)用A表示├A不成立第3章邏輯系形式可推演性(3)命題邏輯中的形式推演規(guī)則都包括在一階邏輯當中,但是其中出現(xiàn)的公式是一階語言中的公式,另外增加了關于量詞的規(guī)則(一階邏輯)形式可推演性:在一階邏輯中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應用一階邏輯的形式推演規(guī)則生成形式推演的例子可以參考本章后面列出的3本關于邏輯的教科書第3章邏輯系統(tǒng)97形式可推演性(3)命題邏輯中的形式推演規(guī)則都包括在一階邏輯當F2形式系統(tǒng)的語義第3章邏輯系統(tǒng)98F2形式系統(tǒng)的語義第3章邏輯系統(tǒng)98形式系統(tǒng)的語義(1)語義即對形式語言進行解釋研究可推導性即形式推演(├)時不考慮作為前提和結(jié)論的命題的內(nèi)容,只考慮命題真假并由此確定前提的真是否蘊涵結(jié)論的真,即前提和結(jié)論之間是否有可推導關系(語法)研究形式系統(tǒng)的語義時,對形式系統(tǒng)賦予研究對象的集合即論域;用論域中的個體對象、對象之上的運算(函數(shù))、對象之間的關系(謂詞)去解釋形式系統(tǒng)中的符號,稱作指稱denote指稱語義學第3章邏輯系統(tǒng)99形式系統(tǒng)的語義(1)語義即對形式語言進行解釋第3章邏輯系統(tǒng)形式系統(tǒng)的語義(2)賦予形式系統(tǒng)的論域及解釋稱為形式系統(tǒng)的語義結(jié)構(gòu),簡稱結(jié)構(gòu)(structure)/結(jié)構(gòu)及其在該結(jié)構(gòu)下公式所取真值的規(guī)定,稱為形式系統(tǒng)的指稱語義(denotationalsemantics)第3章邏輯系統(tǒng)100形式系統(tǒng)的語義(2)賦予形式系統(tǒng)的論域及解釋稱為形式系統(tǒng)的語命題邏輯的可滿足性研究命題邏輯的語義,即研究公式(公式集)的真假賦值問題真假賦值:真假賦值是以所有命題符號的集合為定義域,以真假值{1,0}為值域的函數(shù)。真假賦值v給公式A指派的值記作Av可滿足性:是可滿足的,當且僅當有真假賦值v,使得v=1。此時稱v滿足。第3章邏輯系統(tǒng)101命題邏輯的可滿足性研究命題邏輯的語義,即研究公式(公式集)的可滿足性的可滿足性蘊涵了中所有公式的可滿足性,但反過來不成立。因為這要求同一個真假賦值滿足所有的公式(并非所有可滿足的公式使用同一個賦值)重言式和矛盾式A是重言式(永真式),當且僅當對于任意的真假賦值v,Av=1A是矛盾式(永假式),當且僅當對于任意的真假賦值v,Av=0第3章邏輯系統(tǒng)102可滿足性的可滿足性蘊涵了中所有公式的可滿足性,但反過來不真假判斷與邏輯推論一個命題公式是重言式或者是矛盾式或者兩者都不是,需要進行判定。判定方法可通過構(gòu)造真假值表方法或采用樹形分支的方法來判定可推導關系研究前提的真是否蘊涵結(jié)論的真,引入語義以后對公式進行真假賦值;如果對任意的真假賦值,都有上述關系,則說明前提和結(jié)論之間存在一種邏輯推論關系(或稱邏輯蘊涵)。此時對關系陳述得也更精確第3章邏輯系統(tǒng)103真假判斷與邏輯推論一個命題公式是重言式或者是矛盾式或者兩者都命題邏輯的邏輯推論邏輯推論:設、A分別是命題邏輯中的公式集合和公式,A是的邏輯推論,記為A,當且僅當對于任意真假賦值v,v=1蘊涵Av=1。|=可讀作“邏輯地蘊涵”,|=是前提和結(jié)論A之間的關系,但不是命題語言中的符號,|=A是元語言中的命題第3章邏輯系統(tǒng)104命題邏輯的邏輯推論邏輯推論:設、A分別是命題邏輯中的公式集邏輯推論的證明邏輯推論的證明要證明|=A時,即要證明對于任何真假賦值v,如果v=1則Av=1但任意的真假賦值難于驗證故使用反證法,假設|≠A,即存在一個真假賦值v,使得v=1且Av=0,由此而產(chǎn)生矛盾,即肯定了|=A第3章邏輯系統(tǒng)105邏輯推論的證明邏輯推論的證明第3章邏輯系統(tǒng)105一階語言的語義(1)一階語言的語義:一階語言的解釋包括一個論域和一個函數(shù),函數(shù)把一階語言中的個體符號、n元關系符號(即謂詞)、m元函數(shù)符號分別映射到論域中的個體、論域上的n元關系和m元全函數(shù),是在這個論域中對一階語言的解釋第3章邏輯系統(tǒng)106一階語言的語義(1)一階語言的語義:一階語言的解釋包括一個論一階語言的語義(2)如果n元關系符號和m元函數(shù)中不含自由變量,其項為論域中的個體ai,則原子公式F(t1,…,tn)被解釋為:a1,…,an有R關系;項f(t1,…,tn)被解釋為論域中的個體f(a1,…,an)對于含有自由變量的函數(shù)(項)和公式,則分別被解釋為論域上的m元函數(shù)和n元命題函數(shù),它們經(jīng)過解釋,再給其中的自由變量符號指派論域中的某些個體,就得到論域中個體作為其值、真或假的命題作為其真假值第3章邏輯系統(tǒng)107一階語言的語義(2)如果n元關系符號和m元函數(shù)中不含自由變量一階語言的賦值(1)賦值:一階語言L的賦值v包括一個論域和一個函數(shù),記作v,以L中所有個體符號a、關系符號F、函數(shù)符號f和自由變量符號u構(gòu)成的集合為定義域,且分別把v(a)、v(F)、v(f)、v(u)寫作av、Fv、fv、uv,則有
(1)av,uv∈D (2)FvDn (3)fv:Dm→D第3章邏輯系統(tǒng)108一階語言的賦值(1)賦值:一階語言L的賦值v包括一個論域和一一階語言的賦值(2)項的值:在以D為論域的賦值v之下的項的值遞歸定義如下:
(1)av,uv∈D (2)f(t1,…,tn)v=fv(t1v,…,tnv)對于一階語言的項t,設v是以D為論域的賦值,則tv∈D第3章邏輯系統(tǒng)109一階語言的賦值(2)項的值:在以D為論域的賦值v之下的項的值一階邏輯的邏輯推論公式的真假值:一階語言的公式在以D為論域的賦值之下,其真假值可以遞歸定義一階邏輯的邏輯推論:與命題邏輯相同,只是這里不使用真假賦值,而用賦值邏輯推論:設、A分別是一階語言的公式集和公式,A是的邏輯推論,記作|=A,當且僅當對于任何賦值v,v=1蘊涵Av=1第3章邏輯系統(tǒng)110一階邏輯的邏輯推論公式的真假值:一階語言的公式在以D為論域的邏輯推論的證明方法一階邏輯的邏輯推論證明方法類似于命題邏輯,常用反證法。但對于否證邏輯推論,則需要構(gòu)造賦值所需的論域。確定論域時,關鍵在于論域的大小第3章邏輯系統(tǒng)111邏輯推論的證明方法一階邏輯的邏輯推論證明方法類似于命題邏輯,F(xiàn)3形式系統(tǒng)的整體特征第3章邏輯系統(tǒng)112F3形式系統(tǒng)的整體特征第3章邏輯系統(tǒng)112形式系統(tǒng)的整體特征在經(jīng)典邏輯的形式系統(tǒng)中,形式推演是語法概念,邏輯推論是語義概念形式系統(tǒng)的整體特征:是在形式系統(tǒng)引入語義以后,研究對于任何一階語言的公式集和公式A在何種賦值的條件下,其結(jié)果是否為真/研究形式推演與邏輯推論間的關系賦值的條件:給定某個賦值—可滿足性給定任意賦值—有效性第3章邏輯系統(tǒng)113形式系統(tǒng)的整體特征在經(jīng)典邏輯的形式系統(tǒng)中,形式推演是語法概念可靠性定理與完備性定理對于任何一階語言的公式集和公式A,├A|=A表示:凡是形式可推演性所反映的前提和結(jié)論之間的關系,在非形式的推理中都是成立的,即形式可推演性對于反映非形式的推理是可靠的,此即可靠性定理(或者稱合理性)|=A├
A表示:凡是在非形式推理中成立的前提和結(jié)論之間的關系,形式可推演性都是能夠反映的,即形式可推演性在反映非形式推理時沒有遺漏,此即完備性定理第3章邏輯系統(tǒng)114可靠性定理與完備性定理對于任何一階語言的公式集和公式A,第可滿足性與有效性(1)下面給出有關定義和定理,但均不加證明可滿足性—一階邏輯公式集合是可滿足的,當且僅當有(以某個不空集為論域)賦值v,使得v=1/當v=1時,稱v滿足反過來,不可滿足性就是對任意論域上的任意賦值都有v=0第3章邏輯系統(tǒng)115可滿足性與有效性(1)下面給出有關定義和定理,但均不加證明第可滿足性與有效性(2)有效性:一階邏輯公式A是有效的,當且僅當對于(以任何不空集為論域)任何賦值v,Av=1/有效性也稱為普遍有效性論域中的可滿足性、有效性:(1)在D中是可滿足的,當且僅當有以D為論域的賦值v,使得v=1(2)A在D中是有效的,當且僅當對于任何以D為論域的賦值v,Av=1第3章邏輯系統(tǒng)116可滿足性與有效性(2)有效性:一階邏輯公式A是有效的,當且僅可滿足性與有效性(3)(關于命題的)定理:(1)A是可滿足的,當且僅當?A是不有效的;(2)A是有效的,當且僅當?A是不可滿足的。(關于一階的)定理:(1)A(u1,…,un)是可滿足的,當且僅當x1...xnA(x1,…,xn)是可滿足的(2)A(u1,…,un)是有效的,當且僅當x1...xnA(x1,…,xn)是有效的第3章邏輯系統(tǒng)117可滿足性與有效性(3)(關于命題的)定理:(1)A是可滿足可滿足性與有效性(4)定理:設Form(L),A∈Form(L),和A不含相等符號,D和D1是論域,且|D|≤|D1|,則 (1)如果在D中是可滿足的,則在D1中是可滿足的;(2)如果A在D1中是有效的,則在D中是有效的第3章邏輯系統(tǒng)118可滿足性與有效性(4)定理:設Form(L),A∈Fo可靠性定理(1)可靠性定理[1]:設Form(L),A∈Form(L)(也包括了命題語言Lp) (1)如果├A,則|=A; (2)如果├A,則|=A(即所有形式可推演的都是有效的)第3章邏輯系統(tǒng)119可靠性定理(1)可靠性定理[1]:設Form(L),A∈可靠性定理(2)協(xié)調(diào)性:Form(L)是協(xié)調(diào)的,當且僅當不存在A∈Form(L),使得├A且├?A可靠性定理[2]:設Form(L),A∈Form(L) (1)如果是可滿足的,則是協(xié)調(diào)的; (2)如果A是可滿足的,則A是協(xié)調(diào)的。上述2個定理是等價的,即用可滿足性和協(xié)調(diào)性來陳述可靠性第3章邏輯系統(tǒng)120可靠性定理(2)協(xié)調(diào)性:Form(L)是協(xié)調(diào)的,當且僅完備性定理(1)命題邏輯的完備性定理[1]:設Form(Lp),A∈Form(Lp) (1)如果是協(xié)調(diào)的,則是可滿足的; (2)如果A是協(xié)調(diào)的,則A是可滿足的。定理[2]:設Form(Lp),A∈Form(Lp) (1)如果|=A,則├A; (2)如果|=A,則├A(所有重言式都是形式可證明公式)第3章邏輯系統(tǒng)121完備性定理(1)
溫馨提示
- 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
- 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權益歸上傳用戶所有。
- 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預覽,若沒有圖紙預覽就沒有圖紙。
- 4. 未經(jīng)權益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
- 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負責。
- 6. 下載文件中如有侵權或不適當內(nèi)容,請與我們聯(lián)系,我們立即糾正。
- 7. 本站不保證下載資源的準確性、安全性和完整性, 同時也不承擔用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。
最新文檔
- 2025年水電設施運行維護與保養(yǎng)服務協(xié)議3篇
- 二零二五版清潔能源儲能技術研發(fā)投資分紅合同3篇
- 人教部編版九年級語文下冊-第1課-祖國啊我親愛的祖國【課件】
- 二零二五版計算機配件銷售及售后服務合同3篇
- 2025年企業(yè)創(chuàng)新專利合作協(xié)議
- 2025年人才培養(yǎng)委托合同
- 2025年兒科保健協(xié)議
- 2025年勞務派遣員工協(xié)議范本
- 太陽能光伏發(fā)電站建設施工合同(2025版)2篇
- 2025年咖啡連鎖店競業(yè)禁止協(xié)議
- 物業(yè)民法典知識培訓課件
- 2023年初中畢業(yè)生信息技術中考知識點詳解
- 2024-2025學年山東省德州市高中五校高二上學期期中考試地理試題(解析版)
- 《萬方數(shù)據(jù)資源介紹》課件
- 麻風病病情分析
- TSGD7002-2023-壓力管道元件型式試驗規(guī)則
- 2024年度家庭醫(yī)生簽約服務培訓課件
- 建筑工地節(jié)前停工安全檢查表
- 了不起的狐貍爸爸-全文打印
- 春節(jié)新年紅燈籠中國風信紙
- 注塑件生產(chǎn)通用標準
評論
0/150
提交評論