ch9 一階邏輯中的推理 人工智能課程 北大計算機研究所課件

第九章、一階邏輯中的推理命題與一階推理量詞的實例化（和）如何將一階推理簡化為命題推理（命題化）合一與提升構(gòu)造直接用于一階語句的推理規(guī)則前向鏈接反向鏈接Universalinstantiation(UI)Everyinstantiationofauniversallyquantifiedsentenceisentailedbyit:v

α

Subst({v/g},α) foranyvariablevandgroundtermgE.g.,xKing(x)

Greedy(x)Evil(x)yields:King(John)

Greedy(John)

Evil(John)King(Richard)

Greedy(Richard)

Evil(Richard)King(Father(John))

Greedy(Father(John))

Evil(Father(John))...Existentialinstantiation(EI)Foranysentenceα,variablev,andconstantsymbolkthatdoesnotappearelsewhereintheknowledgebase:v

αSubst({v/k},α)E.g.,x

Crown(x)

OnHead(x,John)yields:Crown(C1)

OnHead(C1,John) providedC1isanewconstantsymbol,calledaSkolemconstantReductioncontd.EveryFOLKBcanbepropositionalizedsoastopreserveentailment（中文書翻譯不準(zhǔn)確?。?AgroundsentenceisentailedbynewKBiffentailedbyoriginalKB)Idea:propositionalizeKBandquery,applyresolution,returnresultProblem:withfunctionsymbols,thereareinfinitelymanygroundterms,e.g.,Father(Father(Father(John)))Reductioncontd.Theorem:Herbrand(1930).IfasentenceαisentailedbyanFOLKB,itisentailedbyafinitesubsetofthepropositionalizedKBIdea:Forn=0to∞docreateapropositionalKBbyinstantiatingwithdepthntermsseeifαisentailedbythisKBProblem:worksifαisentailed,loopsifαisnotentailedTheorem:Turing(1936),Church(1936)EntailmentforFOLis

semidecidable(algorithmsexistthatsayyestoeveryentailedsentence,butnoalgorithmexiststhatalsosaysnotoeverynonentailedsentence.)Problemswith

propositionalizationPropositionalizationseemstogeneratelotsofirrelevantsentences.E.g.,from:xKing(x)Greedy(x)Evil(x)King(John)yGreedy(y)Brother(Richard,John)itseemsobviousthatEvil(John),butpropositionalizationproduceslotsoffactssuchasGreedy(Richard)thatareirrelevantWithpk-arypredicatesandnconstants,therearep·nkinstantiations.第九章、一階邏輯中的推理命題與一階推理量詞的實例化（和）如何將一階推理簡化為命題推理（命題化）合一與提升構(gòu)造直接用于一階語句的推理規(guī)則前向鏈接反向鏈接歸結(jié)GeneralizedModusPonensp1',p2',…,pn',(p1

p2

…pn

q)subst(q,θ)p1'isKing(John) p1isKing(x)p2'isGreedy(y) p2isGreedy(x)θis{x/John,y/John} qisEvil(x)subst(q,θ)isEvil(John)GMPusedwithKBofdefiniteclauses(exactlyonepositiveliteral)AllvariablesassumeduniversallyquantifiedGMPiscalledaliftedversionofModusPonenswheresubst(pi‘,θ)=subst(pi,

θ)foralliUnificationLiftedinferencerulesrequirefindingsubstitutionsthatmakedifferentlogicalexpressionslookidentical.Thisprocessiscalledunification.Unify(α,β)=θifsubst(α,θ)=subst(β,θ)

p q θ

Knows(John,x) Knows(John,Jane) {x/Jane}}Knows(John,x) Knows(y,OJ) {x/OJ,y/John}}Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}}Knows(John,x) Knows(x,OJ) {fail}Standardizingaparteliminatesoverlapofvariables,e.g.,Knows(z17,OJ)AlgorithmforfindingMGU在復(fù)合表達式如F(A,B)中，函數(shù)OP提取函數(shù)符F，ARGS提取參數(shù)表(A,B)。Algorithm(contd)OCCUR-CHECK：當(dāng)將一個變量和一個復(fù)合過程進行匹配時，必須檢查該變量是否在該項中出現(xiàn)。第九章、一階邏輯中的推理命題與一階推理量詞的實例化（和）如何將一階推理簡化為命題推理（命題化）合一與提升構(gòu)造直接用于一階語句的推理規(guī)則前向鏈接反向鏈接歸結(jié)ExampleknowledgebaseThelawsaysthatitisacrimeforanAmericantosellweaponstohostilenations.ThecountryNono,anenemyofAmerica,hassomemissiles,andallofitsmissilesweresoldtoitbyColonelWest,whoisAmerican.ProvethatCol.WestisacriminalExampleknowledgebasecontd....itisacrimeforanAmericantosellweaponstohostilenations:American(x)Weapon(y)Sells(x,y,z)Hostile(z)Criminal(x)Nono…h(huán)assomemissiles,i.e.,xOwns(Nono,x)Missile(x):Owns(Nono,M1)andMissile(M1)…allofitsmissilesweresoldtoitbyColonelWestMissile(x)Owns(Nono,x)Sells(West,x,Nono)Missilesareweapons:Missile(x)Weapon(x)AnenemyofAmericacountsas"hostile“:Enemy(x,America)Hostile(x)West,whoisAmerican…American(West)ThecountryNono,anenemyofAmerica…Enemy(Nono,America)ForwardchainingproofForwardchainingproofPropertiesofforwardchainingSoundandcompleteforfirst-orderdefiniteclausesDatalog（數(shù)據(jù)日志）=first-orderdefiniteclauses+nofunctionsFCterminatesforDataloginfinitenumberofiterationsMaynotterminateingeneralifαisnotentailedThisisunavoidable:entailmentwithdefiniteclausesissemidecidable前向鏈接算法中可能的復(fù)雜性來源算法的“內(nèi)循環(huán)”涉及尋找所有可能的合一者，把規(guī)則的前提與知識庫中一個適合的事實集進行合一（模式匹配），成本可能很高。算法每次遍歷都要對每條規(guī)則進行重新檢查，即使每次遍歷添加到知識庫的規(guī)則很少。算法可能生成許多與目標(biāo)無關(guān)的事實模式匹配和約束滿足之間的聯(lián)系Colorable()isinferredifftheCSPhasasolutionCSPsinclude3SATasaspecialcase,hencematchingisNP-hardDiff(wa,nt)Diff(wa,sa)Diff(nt,q)Diff(nt,sa)Diff(q,nsw)Diff(q,sa)

Diff(nsw,v)Diff(nsw,sa)

Diff(v,sa)Colorable()Diff(Red,Blue) Diff(Red,Green)Diff(Green,Red)Diff(Green,Blue)Diff(Blue,Red) Diff(Blue,Green)增量前向鏈接Noneedtomatcharuleoniterationkifapremisewasn'taddedoniterationk-1matcheachrulewhosepremisecontainsanewlyaddedpositiveliteral無關(guān)的事實：解決辦法采用反向鏈接把前向鏈接限制在一個選定的規(guī)則子集內(nèi)在演繹數(shù)據(jù)庫內(nèi)，利用從目標(biāo)得到的信息重寫規(guī)則集，從而在向前推理過程中只考慮相關(guān)的變量綁定。（魔法集方法，介于前向推理和反向預(yù)處理之間）BackwardchainingalgorithmSUBST(COMPOSE(θ1,θ2),p)=SUBST(θ2,SUBST(θ1,p))BackwardchainingexampleBackwardchainingexampleBackwardchainingexampleBackwardchainingexampleBackwardchainingexampleBackwardchainingexampleBackwardchainingexamplePropertiesofbackwardchainingDepth-firstrecursiveproofsearch:spaceislinearinsizeofproofIncompleteduetoinfiniteloopsfixbycheckingcurrentgoalagainsteverygoalonstackInefficientduetorepeatedsubgoals(bothsuccessandfailure)fixusingcachingofpreviousresults(extraspace)WidelyusedforlogicprogrammingLogicprogramming:PrologAlgorithm=Logic+ControlBasis:backwardchainingwithHornclauses+bells&whistles WidelyusedinEurope,Japan(basisof5thGenerationproject) Compilationtechniques60millionLIPSProgram=setofclauses=head:-literal1,…literaln.criminal(X):-american(X),weapon(Y),sells(X,Y,Z),hostile(Z).Depth-first,left-to-rightbackwardchaining