人工智能原理第3章邏輯系統(tǒng)_第1頁
人工智能原理第3章邏輯系統(tǒng)_第2頁
人工智能原理第3章邏輯系統(tǒng)_第3頁
人工智能原理第3章邏輯系統(tǒng)_第4頁
人工智能原理第3章邏輯系統(tǒng)_第5頁
已閱讀5頁,還剩117頁未讀, 繼續(xù)免費閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進行舉報或認領(lǐng)

文檔簡介

人工智能原理

第3章規(guī)律系統(tǒng)1 本章內(nèi)容

3.1命題規(guī)律和一階謂詞規(guī)律

3.2規(guī)律系統(tǒng)的語法和語義

3.3規(guī)律推理舉例

3.4規(guī)律智能體的推理策略

參考書目

附錄形式系統(tǒng)簡介第3章規(guī)律系統(tǒng)2經(jīng)典數(shù)理規(guī)律AI爭論內(nèi)容之一是推理,即爭論怎樣使計算機獲得自動推理的力量數(shù)理規(guī)律用數(shù)學(xué)方法爭論各種推理中的規(guī)律問題,以推理本身作為爭論對象AI要使用規(guī)律推理,就必定涉及數(shù)理規(guī)律/數(shù)理規(guī)律的經(jīng)典局部—經(jīng)典的命題規(guī)律和一階謂詞規(guī)律,同時作為人工智能的學(xué)問表示方法和推理方法而存在;因此數(shù)理規(guī)律是人工智能的一個根底第3章規(guī)律系統(tǒng)3規(guī)律智能體基于學(xué)問的智能體的核心部件是學(xué)問庫,當這些學(xué)問以規(guī)律形式表示并進展相應(yīng)的推理時,就是規(guī)律智能體學(xué)問表示:命題規(guī)律、一階謂詞規(guī)律推理(一階謂詞規(guī)律)—主要有3類推理算法:前向鏈接和演繹系統(tǒng)、反向鏈接和規(guī)律程序設(shè)計(本章)、歸結(jié)反演和定理證明系統(tǒng)(第4章)承受命題和謂詞演算進展推理的系統(tǒng)(如演繹系統(tǒng))是一種典型的規(guī)律智能體第3章規(guī)律系統(tǒng)43.1命題規(guī)律和一階謂詞規(guī)律

命題、真值、原子公式、合式公式

謂詞、論域、個體

量詞、變量、函數(shù)

一階語言、一階語言的項第3章規(guī)律系統(tǒng)5命題命題:描述客觀世界的可區(qū)分真假的陳述句,即推斷〔經(jīng)典二值規(guī)律:非真即假〕是命題的例子:2+2=4/二月份有30天/2023年哈爾濱有地震/人類能夠證明數(shù)論中全部論斷非真即假〔有待時間〕不是命題的例子:張三比李四聰明/公共汽車內(nèi)特別擁擠〔各人生疏不同〕第3章規(guī)律系統(tǒng)6命題變量與真值命題變量〔變元〕:一個命題用符號表示,稱為命題符號當命題符號代表任一個命題時,即為命題變量真值:真或假–一個命題或命題變量具有真值真值連接詞〔5個〕:否認/合取/析取/蘊涵/等價第3章規(guī)律系統(tǒng)7簡潔命題與復(fù)合命題真值函數(shù):真值聯(lián)結(jié)詞可以視為一元或二元映射(真值函數(shù)),¬是從{T,F}到{T,F},其余是{T,F}2到{T,F}的映射/其函數(shù)定義由真值表確定簡潔命題:一個被視為整體的、具有真或假的命題是簡潔命題;復(fù)合命題:使用聯(lián)結(jié)詞將簡潔命題聯(lián)結(jié)起來的命題是復(fù)合命題第3章規(guī)律系統(tǒng)8命題語言與原子公式命題規(guī)律:爭論復(fù)合命題之間的推導(dǎo)關(guān)系命題語言:是命題規(guī)律使用的形式語言,是符號的集合,用Lp表示/包括:命題符號、連接詞、左右括號原子公式:命題語言中的一個表達式是原子公式,當且僅當它是一個命題符號/原子公式也稱為文字(包括正文字和負文字)第3章規(guī)律系統(tǒng)9命題規(guī)律的合式公式合式公式(well-formedformula),簡稱公式,記作wff:一個表達式是一個公式,當且僅當它能通過有限次地使用下述步驟生成:(1)原子公式是公式;(2)假設(shè)A是公式,則(¬A)是公式;(3)假設(shè)A、B均為公式,則A*B是公式,其中*表示∧∨→≡中的任意一個/公式的形成規(guī)章/命題規(guī)律的主要爭論對象是公式第3章規(guī)律系統(tǒng)10謂詞從命題到一階謂詞:命題內(nèi)部規(guī)律構(gòu)造的分解對推斷的分解,把推斷中的具體內(nèi)容抽出,稱為個體;剩下的推斷即為謂詞謂詞可看作是從個體域或個體域的笛卡兒乘積到真值集合{T/F}的映射典型的推理例子:(1)凡人皆有死;(2)蘇格拉底是人;(3)蘇格拉底有死?!踩握撌健矼(x)D(x),M(s)├D(s)第3章規(guī)律系統(tǒng)11論域與個體論域和個體:在一階規(guī)律中,被爭論對象構(gòu)成的非空集稱為論域;論域中的每個元素稱為個體論域例子:前面例子中的論域是“人”/全部的有理數(shù)都是實數(shù):其論域為有理數(shù)一階規(guī)律還爭論個體之間的關(guān)系〔或個體的性質(zhì)〕及作用于個體的函數(shù)論域/個體/個體間關(guān)系/作用于個體函數(shù)這4個成分構(gòu)成了一階規(guī)律的構(gòu)造第3章規(guī)律系統(tǒng)12謂詞謂詞〔關(guān)系〕:一階形式語言中用于指稱論域中個體的性質(zhì)或者個體之間關(guān)系的形式符號〔大寫字母表示〕給定了論域,就確定了謂詞的真假值一元謂詞:個體的性質(zhì);二元謂詞(多元謂詞):個體的關(guān)系個體的位置—空位,具體化—構(gòu)成意義完整的語句空位的數(shù)目—謂詞的元數(shù)→幾元謂詞第3章規(guī)律系統(tǒng)13量詞與變量變量(變元):表示論域內(nèi)的任意一個個體/常量(常元),表示確定的個體量詞與變量:量詞用來表示謂詞的推斷特性全稱量詞:對全部的xxP(x)存在量詞:存在xxP(x)約束變量:、中x的變量,量詞所管轄的公式如P(x)稱為量詞轄域自由變量:不在量詞轄域內(nèi)的變量為自由變量第3章規(guī)律系統(tǒng)14約束變量和自由變量區(qū)分:自由變量可代入常量,約束變量不行,由于aP(a)無意義;約束變量可改名,自由變量不行帶有全稱變量x的命題表示為一階公式時,其表示形式為x(P(x)→…),帶有存在變量x的命題則表示形式為x(P(x)∧…)例子:全部有理數(shù)都是實數(shù)x(P(x)→R(x)),有些人身超群過2米x(M(x)∧G(x))上述使用方式不行轉(zhuǎn)變,否則造成規(guī)律錯誤第3章規(guī)律系統(tǒng)15函數(shù)函數(shù):表示個體之間的運算,可作用于一個或數(shù)個個體〔用小寫字母〕給定一個或假設(shè)干個體〔對象〕,產(chǎn)生一個新的個體〔對象〕/函數(shù)的元數(shù)例子:x的父親father(張三)兩數(shù)之和仍是一個數(shù)add(e1,e2)第3章規(guī)律系統(tǒng)16函數(shù)與謂詞的區(qū)分謂詞和函數(shù)的區(qū)分:謂詞代表語句,結(jié)果是關(guān)系〔具有真假值〕;函數(shù)代表關(guān)系運算,結(jié)果是一個新個體例子:謂詞SUM(e1,e2,e3)說明e1、e2、e3之間的關(guān)系是e1與e2的和是e3,函數(shù)add(e1,e2)說明e1與e2相加的結(jié)果仍是一個數(shù)第3章規(guī)律系統(tǒng)17一階語言(1)一階語言L:是一階規(guī)律使用的形式語言,可以和任何構(gòu)造〔論域〕沒有聯(lián)系,也可以與某個構(gòu)造有聯(lián)系與構(gòu)造沒有聯(lián)系的一階語言由8類符號組成:(1)無限序列的個體符號〔個體常量〕(2)無限序列的謂詞符號,有確定的元數(shù)n≥1有一個特殊的謂詞符號稱為相等符號〔等式〕,記為=。L可含或不含=,假設(shè)含有,即稱為含=的一階規(guī)律第3章規(guī)律系統(tǒng)18一階語言(2)(3)無限序列的函數(shù)符號,有確定的元數(shù)m≥1(4)無限序列的自由變量:用u/v/w等表示自由變量(5)無限序列的約束變量:用x/y/z等表示約束變量(6)聯(lián)結(jié)詞:¬∧∨→≡(7)量詞:、(8)標點:左右括號、逗號(),第3章規(guī)律系統(tǒng)19一階語言的項和公式L的項:一階語言中的一個符號是項t,當且僅當它能通過有限次使用下述步驟生成: (1)個體常量、自由變量是項; (2)假設(shè)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章規(guī)律系統(tǒng)20一階語言的公式(1)L的公式:一階語言中的一個表達式是一個公式,當且僅當它能通過有限次使用下述步驟生成:(1)原子公式是公式;(2)假設(shè)A是公式,則(¬A)是公式;(3)假設(shè)A、B均為公式,則A*B是公式,其中*表示∧∨→≡中的任意一個(4)假設(shè)A(u)是公式,且x不在A(u)中消失,則xA(x)、xA(x)都是公式第3章規(guī)律系統(tǒng)21一階語言的公式(2)一階謂詞公式的例子數(shù)學(xué)命題的表示:5只被1和5整除設(shè)Q(x,y)表示x被y整除,N(x)表示x是自然數(shù)x(Q(5,x)→N(5)∨N(1))自然語言語句的表示:他不能在全部時刻哄騙全部人設(shè)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章規(guī)律系統(tǒng)223.2規(guī)律系統(tǒng)的語法和語義

規(guī)律系統(tǒng)的語法

規(guī)律系統(tǒng)的語義

語法和語義之間的關(guān)系第3章規(guī)律系統(tǒng)23規(guī)律系統(tǒng)規(guī)律系統(tǒng)(亦稱形式系統(tǒng)FormalSystem)由5個局部組成:符號表—非空集合,即規(guī)律(形式)語言—如一階語言上全體符號的集合*的子集—項和變量*的子集—公式|公式和項的交集為空公式FORMULA上的子集—公理AXIOM公式上的n元關(guān)系集合—推理規(guī)章RULE、項TERM、FORMULA稱為FS的組成局部/AXIOM、RULE稱為FS的推演局部第3章規(guī)律系統(tǒng)24語法和形式推演規(guī)律系統(tǒng)除符號表以外的局部構(gòu)成了規(guī)律系統(tǒng)的語法形式推演:定義了公式之間的形式可推演性關(guān)系,它涉及公式的語法構(gòu)造,其正確性能夠機械地證明用記號├表示形式可推演關(guān)系,讀作“推出”用├A表示A是由形式可推演的〔或形式可證明的〕,其中是前提,A是結(jié)論第3章規(guī)律系統(tǒng)25推演規(guī)章舉例形式推演由形式推演規(guī)章定義,舉例如下:自反 A├A (Ref)傳遞 if├‘├Athen├A ()¬消去(反證律) if,¬A├B&,¬A├¬B then├A (¬–)公式變換 A→BAB第3章規(guī)律系統(tǒng)26形式可推演性形式可推演性:在命題/一階規(guī)律系統(tǒng)中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應(yīng)用相應(yīng)規(guī)律的形式推演規(guī)章生成即├A成立,當且僅當存在有限序列使得1├A1,2├A2,…,n├An中的每一項均由某個形式推導(dǎo)規(guī)章生成,且n├An就是├A即n=,An=A建立在上述形式推演規(guī)章根底上的形式推演系統(tǒng)稱為自然推演(演繹)系統(tǒng)第3章規(guī)律系統(tǒng)27規(guī)律系統(tǒng)的語義語義即對形式語言進展解釋爭論可推導(dǎo)性即形式推演(├)時不考慮作為前提和結(jié)論的命題的內(nèi)容,只考慮命題真假并由此確定前提的真是否蘊涵結(jié)論的真,即前提和結(jié)論之間是否有可推導(dǎo)關(guān)系(語法)爭論形式系統(tǒng)的語義時,對規(guī)律系統(tǒng)賜予爭論對象的集合即論域;用論域中的個體對象、對象之上的運算(函數(shù))、對象之間的關(guān)系(謂詞)去解釋規(guī)律系統(tǒng)中的符號,稱作指稱denote指稱語義學(xué)賜予形式系統(tǒng)的論域及解釋稱為形式系統(tǒng)的語義構(gòu)造,簡稱構(gòu)造(structure)第3章規(guī)律系統(tǒng)28命題規(guī)律的語義與可滿足性爭論命題規(guī)律的語義,即爭論公式(公式集)的真假賦值問題真假賦值:真假賦值是以全部命題符號的集合為定義域、以真假值{1,0}為值域的函數(shù)。真假賦值v給公式A指派的值記作Av可滿足性:是可滿足的,當且僅當有真假賦值v,使得v=1。此時稱v滿足。第3章規(guī)律系統(tǒng)29可滿足性的可滿足性蘊涵了中全部公式的可滿足性,但反過來不成立。由于這要求同一個真假賦值滿足全部的公式(并非全部可滿足的公式使用同一個賦值)重言式和沖突式A是重言式(永真式),當且僅當對于任意的真假賦值v,Av=1A是沖突式(永假式),當且僅當對于任意的真假賦值v,Av=0第3章規(guī)律系統(tǒng)30真假推斷與規(guī)律推論一個命題公式是重言式或者是沖突式或者兩者都不是,需要進展判定。判定方法可通過構(gòu)造真假值表方法或承受樹形分支的方法來判定可推導(dǎo)關(guān)系:爭論前提的真是否蘊涵結(jié)論的真,引入語義以后對公式進展真假賦值;假設(shè)對任意的真假賦值,都有上述關(guān)系,則說明前提和結(jié)論之間存在一種規(guī)律推論關(guān)系(或稱規(guī)律蘊涵)第3章規(guī)律系統(tǒng)31命題規(guī)律的規(guī)律推論規(guī)律推論:設(shè)、A分別是命題規(guī)律中的公式集合和公式,A是的規(guī)律推論,記為A,當且僅當對于任意真假賦值v,v=1蘊涵Av=1。|=可讀作“規(guī)律地蘊涵”,|=是前提和結(jié)論A之間的關(guān)系規(guī)律推論的證明要證明|=A時,即要證明對于任何真假賦值v,假設(shè)v=1則Av=1(通常使用反證法)第3章規(guī)律系統(tǒng)32一階語言的語義一階語言的語義:一階語言的解釋包括一個論域和一個函數(shù)函數(shù)把一階語言中的個體符號映射到論域中的個體n元關(guān)系符號(即謂詞)映射到論域上的n元關(guān)系m元函數(shù)符號映射到論域上的m元全函數(shù)以上組成了該論域中對一階語言的解釋第3章規(guī)律系統(tǒng)33一階語言的賦值賦值:一階語言L的賦值v包括一個論域D和一個函數(shù)(記作v)L中全部個體符號a為定義域,其賦值v(a)或av關(guān)系符號F的賦值v(F)或Fv函數(shù)符號f的賦值v(f)或fv自由變量符號u的賦值v(u)或uv則有 (1)av,uv∈D (2)FvDn (3)fv:Dm→D第3章規(guī)律系統(tǒng)34一階規(guī)律的規(guī)律推論公式的真假值:一階語言的公式在以D為論域的賦值之下,其真假值可以遞歸定義一階規(guī)律的規(guī)律推論:與命題規(guī)律一樣,只是這里不使用真假賦值,而用賦值規(guī)律推論:設(shè)、A分別是一階語言的公式集和公式,A是的規(guī)律推論,記作|=A,當且僅當對于任何賦值v,v=1蘊涵Av=1一階規(guī)律的規(guī)律推論證明方法類似于命題規(guī)律,常用反證法。但對于否證規(guī)律推論,則需要構(gòu)造賦值所需的論域。確定論域時,關(guān)鍵在于論域的大小第3章規(guī)律系統(tǒng)35規(guī)律系統(tǒng)的整體特征在經(jīng)典規(guī)律的形式系統(tǒng)中,形式推演是語法概念,規(guī)律推論是語義概念形式系統(tǒng)的整體特征:是在形式系統(tǒng)引入語義以后,爭論對于任何一階語言的公式集和公式A在何種賦值的條件下,其結(jié)果是否為真—即爭論形式推演與規(guī)律推論之間的關(guān)系賦值的條件:給定某個賦值—可滿足性給定任意賦值—有效性第3章規(guī)律系統(tǒng)36牢靠性定理與完備性定理對于任何一階語言的公式集和公式A,├A|=A表示:但凡形式可推演性所反映的前提和結(jié)論之間的關(guān)系,在非形式的推理中都是成立的,即形式可推演性對于反映非形式的推理是牢靠的,此即牢靠性定理(或者稱合理性)|=A├A表示:但凡在非形式推理中成立的前提和結(jié)論之間的關(guān)系,形式可推演性都是能夠反映的,即形式可推演性在反映非形式推理時沒有遺漏,此即完備性定理第3章規(guī)律系統(tǒng)37可滿足性與有效性(1)不加證明地給出有關(guān)定義和定理可滿足性—一階規(guī)律公式集合是可滿足的,當且僅當有(以某個不空集為論域)賦值v,使得v=1/當v=1時,稱v滿足反過來,不行滿足性就是對任意論域上的任意賦值都有v=0第3章規(guī)律系統(tǒng)38可滿足性與有效性(2)有效性:一階規(guī)律公式A是有效的,當且僅當對于(以任何不空集為論域)任何賦值v,Av=1/有效性也稱為普遍有效性論域中的可滿足性、有效性:(1)在D中是可滿足的,當且僅當有以D為論域的賦值v,使得v=1(2)A在D中是有效的,當且僅當對于任何以D為論域的賦值v,Av=1第3章規(guī)律系統(tǒng)39可滿足性與有效性(3)(關(guān)于命題的)定理:(1)A是可滿足的,當且僅當?A是不有效的;(2)A是有效的,當且僅當?A是不行滿足的。(關(guān)于一階的)定理:(1)A(u1,…,un)是可滿足的,當且僅當x1...xnA(x1,…,xn)是可滿足的(2)A(u1,…,un)是有效的,當且僅當x1...xnA(x1,…,xn)是有效的第3章規(guī)律系統(tǒng)40牢靠性定理牢靠性定理[1]:設(shè)Form(L),A∈Form(L)(也包括了命題語言Lp) (1)假設(shè)├A,則|=A; (2)假設(shè)├A,則|=A(即全部形式可推演的都是有效的)協(xié)調(diào)性(無沖突性):Form(L)是協(xié)調(diào)的,當且僅當不存在A∈Form(L),使得├A且├?A牢靠性定理[2]:設(shè)Form(L),A∈Form(L) (1)假設(shè)是可滿足的,則是協(xié)調(diào)的; (2)假設(shè)A是可滿足的,則A是協(xié)調(diào)的。([1][2]等價)第3章規(guī)律系統(tǒng)41完備性定理命題規(guī)律和一階規(guī)律的完備性定理[1]:設(shè)Form(L),A∈Form(L)(含Lp) (1)假設(shè)是協(xié)調(diào)的,則是可滿足的; (2)假設(shè)A是協(xié)調(diào)的,則A是可滿足的。定理[2]:設(shè)Form(L),A∈Form(L) (1)假設(shè)|=A,則├A; (2)假設(shè)|=A,則├A(全部有效公式都是形式可證明公式)。假設(shè)對論域限定以后,可得更準確的陳述第3章規(guī)律系統(tǒng)423.3規(guī)律推理舉例

wumpus世界

命題規(guī)律推理模式

基于電路的智能體第3章規(guī)律系統(tǒng)43wumpus世界(1)Wumpus是一個早期電腦玩耍中的怪物Agent感知:陷阱旁邊有微風(fēng)breeze怪獸旁邊有惡臭stench金子閃閃發(fā)光glitter感覺墻的反彈陷阱和怪物的位置隨機生成第3章規(guī)律系統(tǒng)stenchBreezePitWumpus(Monster)BreezeStenchGoldPitBreezestenchBreezeAgentBreezePitBreeze44wumpus世界(2)Wumpus世界搜尋圖示—感知用5元組表示 [感知wumpus,感知微風(fēng),感知金光,感知墻,感知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章規(guī)律系統(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世界(3)1,42,43,44,41,3W!2,33,34,31,2ASOK2,2OK3,24,21,1VOK2,1BVOK3,1P!4,1第3章規(guī)律系統(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世界中的命題和推理規(guī)章只考慮陷阱的狀況Pi,j=T—[i,j]中有陷阱,記為Pi,jBi,j=T—[i,j]中有微風(fēng),記為Bi,j規(guī)章如下:R1 P1,1R2 B1,1P1,2P2,1R3 B2,1P1,1P2,2P3,1R4 B1,1R5 B2,1第3章規(guī)律系統(tǒng)47命題規(guī)律推理模式分別規(guī)章與消去規(guī)律等價(雙向蘊涵消去)第3章規(guī)律系統(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) 逆否命題規(guī)律等價R9 ?(P1,2∨P2,1) R4/R8分別規(guī)章R10(結(jié)果) ?P1,2∧?P2,1 迪摩根定律第3章規(guī)律系統(tǒng)49基于電路的智能體基于電路的智能體的目的:把對現(xiàn)狀的感知變?yōu)橹悄荏w的行動感知=input→推斷/行動推斷:尖叫→怪獸wumpus將死亡行動:金光→抓起金子/行動掌握=存放器第3章規(guī)律系統(tǒng)grabglitter

Alive延遲Scream

50wumpus世界中智能體的推斷(1)位置推斷:在L1,1—分為3種狀況:始終留在[1,1],從[1,2]走到[1,1],從[2,1]走到[1,1]使用位置存放器/狀態(tài)存放器第3章規(guī)律系統(tǒng)L1,2L2,1facing-leftfacing-down∧∧?∧∨∨L1,1forwardbump51wumpus世界中智能體的推斷(2)上述電路圖表示為規(guī)律表達式 第3章規(guī)律系統(tǒng)前述電路的規(guī)律表達式推斷wumpus是否活著覺察金子后的行動但由于沒有變量,不能表示更一般的狀況,如不同位置用同一個規(guī)律式523.4規(guī)律智能體的推理策略

規(guī)律智能體構(gòu)造

Horn子句

置換與合一

前向鏈接算法/后向鏈接算法第3章規(guī)律系統(tǒng)53規(guī)律智能體的構(gòu)造(1)以一階謂詞演算為核心的規(guī)律系統(tǒng)是典型的規(guī)律智能體系統(tǒng)的根底是一階語言,由此構(gòu)造學(xué)問庫/一般構(gòu)造學(xué)問庫(學(xué)問工程)的過程包括:確定任務(wù)收集相關(guān)學(xué)問確定謂詞、函數(shù)和常量詞匯表第3章規(guī)律系統(tǒng)54規(guī)律智能體的構(gòu)造(2)對領(lǐng)域(論域)的通用學(xué)問進展編碼對特定問題實例的描述進展編碼查詢提交、推理、給出答案調(diào)試學(xué)問庫假設(shè)承受一階語言的特殊形式—確定子句Horn子句,可獲得高效推理第3章規(guī)律系統(tǒng)55Horn子句Horn子句(HornClause):是一類至多只有一個正文字的子句(子句=文字的析取式)例子:?A∨?B∨C(留意:這是一般公式AB→C的變形)Horn子句稱為確定子句,其中正文字稱為子句的頭,負文字構(gòu)成子句的體第3章規(guī)律系統(tǒng)56Horn子句的性質(zhì)只有一個正文字的約束具有重要意義:每個Horn子句實際上都是一個蘊涵式的變形,實際學(xué)問庫中常常使用這樣易懂的形式/沒有正文字的Horn子句可以寫成結(jié)論為FALSE的蘊涵式Horn子句的推理可以使用前向鏈接和后向鏈接算法用Horn子句判定蘊涵所需時間與數(shù)據(jù)庫成線性關(guān)系最重要的是最終一共性質(zhì)第3章規(guī)律系統(tǒng)57推理策略簡要介紹2種推理算法—簡潔的前向鏈接算法和簡潔的后向鏈接算法,結(jié)合一個例子說明算法的應(yīng)用一階推理規(guī)章—一般化分別規(guī)章(GeneralizedModusPonens)對于原子語句pi,pi’,q,存在置換,使得(pi)=(pi’),對全部i都成立,則第3章規(guī)律系統(tǒng)58置換與合一置換(或代換):設(shè)x1~xn是n個變量,且各不一樣,t1~tn是n個項(常量、變量、函數(shù)),ti≠xi,則有限序列{t1/x1,t2/x2…tn/xn}稱為一個置換置換乘積(合成):設(shè)和是2個置換,則先后作用于公式或項,稱為置換乘積,用表示。通過相關(guān)的置換,使不同的一階公式成為一樣的,這個過程稱為合一第3章規(guī)律系統(tǒng)59合一置換合一置換:設(shè)有一組謂詞公式{E1~Ek}和置換,使E1=E2=…=Ek,則稱為合一置換,E1~Ek稱為可合一的/合一置換也叫通代最一般合一置換(最廣通代):假設(shè)和都是公式組{E1~Ek}的合一置換,且有置換存在,使得=,則稱為公式組{E1~Ek}的最一般合一置換,記為mgu(mostgeneralunification)第3章規(guī)律系統(tǒng)60置換與合一的例子有子句xKing(x)∧Greedy(x)→Evil(x)King(John)Greedy(John)則做置換={x/John},用一般化分別規(guī)章可得:q=Evil(John)第3章規(guī)律系統(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章規(guī)律系統(tǒng)62用于規(guī)律推理的例子問題描述:美國法律規(guī)定:美國人(American)賣武器(weapon)給敵對國家(hostile)是犯罪的(criminal).美國的敵國Nono有一些(missile),全部這些是West上校賣給他們的,而West上校是一個美國人證明:West是犯罪的第3章規(guī)律系統(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章規(guī)律系統(tǒng)64問題用一階子句表示(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]上述描述放入學(xué)問庫:[1]~[3]為確定子句(上述原始形式均可以化為原子的析取且只有一個正文字),[4]~[7]為正文字第3章規(guī)律系統(tǒng)65前向鏈接算法的說明(1)前向鏈接算法的推理過程:從事實(學(xué)問庫中的原子公式)開頭,依次對學(xué)問庫中的規(guī)章(以確定子句的形式消失)進展置換,檢查規(guī)章前提局部的文字是否全部與學(xué)問庫中的事實相匹配假設(shè)是匹配的,則把該條規(guī)章已經(jīng)做過置換的結(jié)論局部添加到學(xué)問庫中,假設(shè)這個結(jié)論和查詢(既需要推導(dǎo)出的結(jié)論)全都,則推理完畢,獲得證明第3章規(guī)律系統(tǒng)66前向鏈接算法的說明(2)重復(fù)上述過程,直到獲得證明;或者再沒有新的事實(推出的結(jié)論)參加,則此時推理以證明失敗完畢約束:要求每次參加學(xué)問庫的結(jié)論都是全新的,而不是事實的重命名(即謂詞一樣只是變量名不同)第3章規(guī)律系統(tǒng)67簡潔的前向鏈接算法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章規(guī)律系統(tǒng)68前向鏈接算法例子(1)第3章規(guī)律系統(tǒng)使用前向鏈接算法對前面的例子進展推理用學(xué)問庫中的事實(即[4]~[7])依次對學(xué)問庫中的各個子句進展置換操作并用推理規(guī)章獲得新的文字第一次循環(huán)體執(zhí)行:子句[1]前提局部未獲滿足(為什么?)子句[2]—使用置換{x/M1},則可得 Sell(West,M1,Nono) [8]子句[3]—使用置換{x/M1},則可得Weapon(M1) [9]69前向鏈接算法例子(2)第3章規(guī)律系統(tǒng)此時new中為[8][9],為原學(xué)問庫所未有,將它們添加到學(xué)問庫中其次次循環(huán)體執(zhí)行:再次循環(huán)時new首先清空子句[1]—置換{x/West,y/M1,z/Nono} 得到Criminal(West) [10]添加到new中,與查詢進展合一測試,全都則返回/算法完畢70前向鏈接生成的證明樹第3章規(guī)律系統(tǒng)Criminal(West)Weapon(M1)Sells(West,M1,Nono)Hostile(Nono)American(West)Missile(M1)Owns(Nono,M1)Enemy(Nono,America)71反向鏈接算法的說明(1)原始查詢(既要證明的結(jié)論)以目標列表的形式消失,開頭時列表中只有一個元素列表的操作相當于棧,是一個遞歸過程(如下)即深度優(yōu)先的搜尋過程推理過程是從結(jié)論(子句的頭)開頭,找到匹配的頭就擴展這個頭所在的規(guī)章體;擴展局部又作為頭連續(xù)擴展,直到全部原子均與事實相匹配比較:正向=事實結(jié)論/反向=結(jié)論事實第3章規(guī)律系統(tǒng)72反向鏈接算法的說明(2)算法的推理過程是:選取棧當中的第一個目標,在學(xué)問庫中查找子句的頭(即結(jié)論局部)能與目標合一的每個子句每個這樣的子句創(chuàng)立了一個遞歸調(diào)用過程,在這個遞歸調(diào)用過程中子句的前提(子句的體)被參加到目標棧當中當棧中全部目標都得到匹配,則當前的證明分支是成功的留意:事實是指有頭沒有體的子句(正文字)第3章規(guī)律系統(tǒng)73反向鏈接算法的說明(3)在算法中answers作為存放置換的數(shù)據(jù)構(gòu)造,返回一系列置換操作,這些操作說明白反向鏈接算法獵取證明的過程在算法中包括了置換的合成’(或者寫為Compose(’,)),其效果就是依次進展每個置換第3章規(guī)律系統(tǒng)74反向鏈接算法的說明(4)第一次應(yīng)用算法,對于待證明的目標來說,本身就是一個正文字,此時要用這個文字中的常量對適宜的規(guī)章(子句的頭與該文字匹配)進展置換這個置換通過遞歸調(diào)用帶入下一次置換,就得到了合成置換在本例中有:初始{x/West} 遞歸{x/West,y/M1} 遞歸{x/West,y/M1,z/Nono}第3章規(guī)律系統(tǒng)75簡潔的反向鏈接算法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章規(guī)律系統(tǒng)76反向鏈接算法例子(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}匹配,遞歸返回復(fù)合={x/West,y/M1}第3章規(guī)律系統(tǒng)77反向鏈接算法例子(2)再次遞歸調(diào)用Sell(West,M1,z)—得到置換={z/Nono},遞歸返回復(fù)合置換{x/West,y/M1,z/Nono}在置換過程中每個變量只能置換一個常量作為約束,削減置換的不定性此時子目標全部匹配,再無新的子目標生成,返回置換集合完畢第3章規(guī)律系統(tǒng)78反向鏈接生成的證明樹第3章規(guī)律系統(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正向鏈接和反向鏈接前向鏈接算法特點:數(shù)據(jù)驅(qū)動/是牢靠的和完備的后向鏈接算法特點:目標驅(qū)動/是牢靠的但不是完備的(書中p220/p224)可以從“是否能找到問題的解”角度考慮不完備性后向鏈接算法依據(jù)目標來進展相關(guān)事實的匹配,對于大規(guī)模的學(xué)問庫來說有助于減小搜尋空間第3章規(guī)律系統(tǒng)80參考書目StuartRussell/PeterNorvig:AIMA第7章/第8章/第9章陸汝鈐編著:人工智能(上冊)第1章陸鐘萬,面對計算機科學(xué)的數(shù)理規(guī)律,科學(xué)出版社,1998年1月第1版朱梧[木賈]、肖奚安,數(shù)理規(guī)律引論,南京大學(xué)出版社,1995年5月第1版王元元,計算機科學(xué)中的規(guī)律學(xué),科學(xué)出版社,1989年9月第1版第3章規(guī)律系統(tǒng)81附錄形式系統(tǒng)簡介

F1形式系統(tǒng)和形式推演

F2形式系統(tǒng)的語義

F3形式系統(tǒng)的整體特征第3章規(guī)律系統(tǒng)82F1形式系統(tǒng)定義和形式推演第3章規(guī)律系統(tǒng)83形式系統(tǒng)定義(1)規(guī)律的形式系統(tǒng)的定義–一個形式系統(tǒng)FormalSystem由5個局部組成:(1)符號表,非空集合,即形式語言(如Lp和L);(2)上全體符號的集合*的一個子集TERM,其元素稱為FS的項;TERM有子集VARIABLE,其元素稱為變量;(3)*的一個子集FORMULA,其元素稱為FS的公式;FORMULA有子集ATOM,其元素稱為原子公式;TERMFORMULA=;第3章規(guī)律系統(tǒng)84形式系統(tǒng)定義(2)(4)FORMULA的一個子集AXIOM,其元素稱為FS的公理;(5)FORMULA上的n元關(guān)系集合RULE,其元素稱為FS的推理規(guī)章。其中、TERM、FORMULA稱為FS的組成局部,AXIOM、RULE稱為FS的推演局部公理推演系統(tǒng)包括AXIOM,而自然推演系統(tǒng)只包括推理規(guī)章第3章規(guī)律系統(tǒng)85對象語言和元語言(1)對象語言和元語言:作為被爭論對象的語言稱為對象語言,用以爭論對象語言的語言稱為元語言例子:用漢語爭論英語語法,則英語是對象語言,漢語是元語言數(shù)理規(guī)律中的形式系統(tǒng)各有其自身的形式語言如Lp和L,這些是被爭論的對象,因而是對象語言;但為了爭論這些形式系統(tǒng),又必需使用某種語言,那么這種語言便是元語言第3章規(guī)律系統(tǒng)86對象語言和元語言(2)如:“鳥正在飛行”—描述—對象語言;“命題‘鳥正在飛行’真”—對上句的評論—元語言。形式系統(tǒng)的對象語言,其中的符號既是對客觀對象的抽象,用于爭論客觀對象;同時又是一種符號客體,是被爭論的對象第3章規(guī)律系統(tǒng)87對象語言和元語言(3)形式系統(tǒng)的元語言包括:對形式系統(tǒng)中組成成分的稱謂—項、公式、公理等規(guī)律術(shù)語—假設(shè)-那么、當且僅當、存在、全部等對形式系統(tǒng)性質(zhì)〔整體特征〕的描述—如全都性、完備性、可判定性等,該局部最重要元語言中使用的符號:自然語言〔如漢語〕和一些被引進的符號,如:├、|=等未經(jīng)解釋的形式語言可以沒有含義,但元語言必需有其具體含義。第3章規(guī)律系統(tǒng)88元理論元理論是關(guān)于形式系統(tǒng)的理論,包括三局部內(nèi)容:關(guān)于形式系統(tǒng)語法(syntax)的爭論,不涉及具體意義的符號體系,爭論符號串的推演,即形式推演;關(guān)于形式系統(tǒng)語義(semantics)的爭論,爭論形式系統(tǒng)在被作出各種解釋時的性質(zhì);關(guān)于形式系統(tǒng)語法和語義關(guān)系的爭論,特殊是形式系統(tǒng)的性質(zhì),如:合理性、完備性等。第3章規(guī)律系統(tǒng)89形式推演形式推演:定義了公式之間的形式可推演性關(guān)系,它涉及公式的語法構(gòu)造,其正確性能夠機械地證明用記號├表示形式可推演關(guān)系,讀作“推出”用├A表示A是由形式可推演的〔或形式可證明的〕,其中是前提,A是結(jié)論記號├不是形式語言中的符號,├A也不是形式語言中的公式,而是元語言中的命題第3章規(guī)律系統(tǒng)90常用推演規(guī)章(1)形式推演由形式推演的規(guī)章定義命題規(guī)律中有一些常用的推演規(guī)章(規(guī)章模式)確定前提 ifA∈then├A (∈)增加前提 if├Athen,‘├A(+)自反 A├A (Ref)傳遞 if├‘├Athen├A()第3章規(guī)律系統(tǒng)91常用推演規(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章規(guī)律系統(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章規(guī)律系統(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章規(guī)律系統(tǒng)94形式可推演性(1)(命題規(guī)律)形式可推演性:在命題規(guī)律中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應(yīng)用命題規(guī)律的形式推演規(guī)章生成即├A成立,當且僅當存在有限序列使得1├A1,2├A2,…,n├An中的每一項均由某個形式推導(dǎo)規(guī)章生成,且n├An就是├A即n=,An=A第3章規(guī)律系統(tǒng)95形式可推演性(2)用A表示├A不成立用A|-|B表示左右兩邊的公式可以相互推出,稱其為語法等值公式或等值公式建立在上述形式推演規(guī)章根底上的形式推演系統(tǒng)稱為自然推演(演繹)系統(tǒng)第3章規(guī)律系統(tǒng)96形式可推演性(3)命題規(guī)律中的形式推演規(guī)章都包括在一階規(guī)律當中,但是其中消失的公式是一階語言中的公式,另外增加了關(guān)于量詞的規(guī)章(一階規(guī)律)形式可推演性:在一階規(guī)律中,A是由可形式推演的(或形式可證明的),記為├A,當且僅當├A能通過有限次應(yīng)用一階規(guī)律的形式推演規(guī)章生成形式推演的例子可以參考本章后面列出的3本關(guān)于規(guī)律的教科書第3章規(guī)律系統(tǒng)97F2形式系統(tǒng)的語義第3章規(guī)律系統(tǒng)98形式系統(tǒng)的語義(1)語義即對形式語言進展解釋爭論可推導(dǎo)性即形式推演(├)時不考慮作為前提和結(jié)論的命題的內(nèi)容,只考慮命題真假并由此確定前提的真是否蘊涵結(jié)論的真,即前提和結(jié)論之間是否有可推導(dǎo)關(guān)系(語法)爭論形式系統(tǒng)的語義時,對形式系統(tǒng)賜予爭論對象的集合即論域;用論域中的個體對象、對象之上的運算(函數(shù))、對象之間的關(guān)系(謂詞)去解釋形式系統(tǒng)中的符號,稱作指稱denote指稱語義學(xué)第3章規(guī)律系統(tǒng)99形式系統(tǒng)的語義(2)賜予形式系統(tǒng)的論域及解釋稱為形式系統(tǒng)的語義構(gòu)造,簡稱構(gòu)造(structure)/構(gòu)造及其在該構(gòu)造下公式所取真值的規(guī)定,稱為形式系統(tǒng)的指稱語義(denotationalsemantics)第3章規(guī)律系統(tǒng)100命題規(guī)律的可滿足性爭論命題規(guī)律的語義,即爭論公式(公式集)的真假賦值問題真假賦值:真假賦值是以全部命題符號的集合為定義域,以真假值{1,0}為值域的函數(shù)。真假賦值v給公式A指派的值記作Av可滿足性:是可滿足的,當且僅當有真假賦值v,使得v=1。此時稱v滿足。第3章規(guī)律系統(tǒng)101可滿足性的可滿足性蘊涵了中全部公式的可滿足性,但反過來不成立。由于這要求同一個真假賦值滿足全部的公式(并非全部可滿足的公式使用同一個賦值)重言式和沖突式A是重言式(永真式),當且僅當對于任意的真假賦值v,Av=1A是沖突式(永假式),當且僅當對于任意的真假賦值v,Av=0第3章規(guī)律系統(tǒng)102真假推斷與規(guī)律推論一個命題公式是重言式或者是沖突式或者兩者都不是,需要進展判定。判定方法可通過構(gòu)造真假值表方法或承受樹形分支的方法來判定可推導(dǎo)關(guān)系爭論前提的真是否蘊涵結(jié)論的真,引入語義以后對公式進展真假賦值;假設(shè)對任意的真假賦值,都有上述關(guān)系,則說明前提和結(jié)論之間存在一種規(guī)律推論關(guān)系(或稱規(guī)律蘊涵)。此時對關(guān)系陳述得也更準確第3章規(guī)律系統(tǒng)103命題規(guī)律的規(guī)律推論規(guī)律推論:設(shè)、A分別是命題規(guī)律中的公式集合和公式,A是的規(guī)律推論,記為A,當且僅當對于任意真假賦值v,v=1蘊涵Av=1。|=可讀作“規(guī)律地蘊涵”,|=是前提和結(jié)論A之間的關(guān)系,但不是命題語言中的符號,|=A是元語言中的命題第3章規(guī)律系統(tǒng)104規(guī)律推論的證明規(guī)律推論的證明要證明|=A時,即要證明對于任何真假賦值v,假設(shè)v=1則Av=1但任意的真假賦值難于驗證故使用反證法,假設(shè)|≠A,即存在一個真假賦值v,使得v=1且Av=0,由此而產(chǎn)生沖突,即確定了|=A第3章規(guī)律系統(tǒng)105一階語言的語義(1)一階語言的語義:一階語言的解釋包括一個論域和一個函數(shù),函數(shù)把一階語言中的個體符號、n元關(guān)系符號(即謂詞)、m元函數(shù)符號分別映射到論域中的個體、論域上的n元關(guān)系和m元全函數(shù),是在這個論域中對一階語言的解釋第3章規(guī)律系統(tǒng)106一階語言的語義(2)假設(shè)n元關(guān)系符號和m元函數(shù)中不含自由變量,其項為論域中的個體ai,則原子公式F(t1,…,tn)被解釋為:a1,…,an有R關(guān)系;項f(t1,…,tn)被解釋為論域中的個體f(a1,…,an)對于含有自由變量的函數(shù)(項)和公式,則分別被解釋為論域上的m元函數(shù)和n元命題函數(shù),它們經(jīng)過解釋,再給其中的自由變量符號指派論域中的某些個體,就得到論域中個體作為其值、真或假的命題作為其真假值第3章規(guī)律系統(tǒng)107一階語言的賦值(1)賦值:一階語言L的賦值v包括一個論域和一個函數(shù),記作v,以L中全部個體符號a、關(guān)系符號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

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負責。
  • 6. 下載文件中如有侵權(quán)或不適當內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準確性、安全性和完整性, 同時也不承擔用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

評論

0/150

提交評論