X.Firstorderlogic(FOL)

Autumn2012Instructor:WangXiaolongHarbinInstituteofTechnology,ShenzhenGraduateSchoolIntelligentComputationResearchCenter(HITSGSICRC)X.Firstorderlogic(FOL)AOutlineWhyFOL?SyntaxandsemanticsofFOLUsingFOLWumpusworldinFOLKnowledgeengineeringinFOLOutlineWhyFOL?ProsandconsofpropositionallogicPropositionallogicisdeclarativePropositionallogicallowspartial/disjunctive/negatedinformation(unlikemostdatastructuresanddatabases)Propositionallogiciscompositional:meaningofB1,1

P1,2isderivedfrommeaningofB1,1andofP1,2Meaninginpropositionallogiciscontext-independent(unlikenaturallanguage,wheremeaningdependsoncontext)Propositionallogichasverylimitedexpressivepower(unlikenaturallanguage)E.g.,cannotsay"pitscausebreezesinadjacentsquares“exceptbywritingonesentenceforeachsquareProsandconsofpropositionalFirst-orderlogicWhereaspropositionallogicassumestheworldcontainsfactsFirst-orderlogic(likenaturallanguage)assumesacarcontainsObjects:people,houses,numbers,colors,baseballgames,wars,…Relations:red,round,prime,brotherof,biggerthan,partof,comesbetween,…Functions:fatherof,bestfriend,onemorethan,plus,…First-orderlogicWhereaspropoExamples:“Oneplustwoequalsthree” Objects: Relations: Properties: Functions:“SquaresneighboringtheWumpusaresmelly” Objects: Relations: Properties: Functions:Examples:“OneplustwoequalsExamples:“Oneplustwoequalsthree” Objects: one,two,three,oneplustwo Relations: equals Properties: -- Functions: plus(“oneplustwo”isthenameoftheobject obtainedbyapplyingfunctionplustooneandtwo; threeisanothernameforthisobject)“SquaresneighboringtheWumpusaresmelly” Objects: Wumpus,square Relations: neighboring Properties: smelly Functions: --Examples:“OneplustwoequalsSemanticsthereisacorrespondencebetweenfunctions,whichreturnvaluespredicates,whicharetrueorfalseFunction:father_of(Mary)=BillPredicate:father_of(Mary,Bill)SemanticsthereisacorrespondSyntaxofFOL:BasicelementsConstants KingJohn,2,HIT,...Predicates Brother,>,...Functions Sqrt,LeftLegOf,...Variables x,y,a,b,...Connectives ,,,,Equality =Quantifiers ,

SyntaxofFOL:BasicelementsCAtomicsentencesAtomicsentence= predicate(term1,...,termn) orterm1=term2Term = function(term1,...,termn) orconstantorvariable

E.g.,Brother(KingJohn,RichardTheLionheart)>(Length(LeftLegOf(Richard)),Length(LeftLegOf(KingJohn)))AtomicsentencesAtomicsentencComplexsentencesComplexsentencesaremadefromatomicsentencesusingconnectivesS,S1

S2,S1S2,S1

S2,S1

S2,E.g.Sibling(KingJohn,Richard)Sibling(Richard,KingJohn)

>(1,2)≤(1,2)>(1,2)

>(1,2)ComplexsentencesComplexsenteTruthinfirst-orderlogicSentencesaretruewithrespecttoamodelandaninterpretationModelcontainsobjects(domain

elements)andrelationsamongthemInterpretationspecifiesreferentsforconstant

symbols

→

objectspredicate

symbols → relationsfunction

symbols → functionalrelationsAnatomicsentencepredicate(term1,...,termn)istrue ifftheobjectsreferredtobyterm1,...,termn areintherelationreferredtobypredicateTruthinfirst-orderlogicSentModelsforFOL:ExampleModelsforFOL:ExampleUniversalquantification<variables><sentence>EveryoneatHITissmart:xAt(x,HIT)Smart(x)xPistrueinamodelmiffPistruewithxbeingeachpossibleobjectinthemodelRoughlyspeaking,equivalenttotheconjunctionofinstantiationsofP At(KingJohn,HIT)Smart(KingJohn) At(Richard,HIT)Smart(Richard) At(HIT,HIT)Smart(HIT) ...Universalquantification<variAcommonmistaketoavoidTypically,isthemainconnectivewithCommonmistake:usingasthemainconnectivewith:xAt(x,HIT)Smart(x)means“EveryoneisatHITandeveryoneissmart”AcommonmistaketoavoidTypicExistentialquantification<variables><sentence>SomeoneatHITissmart:xAt(x,HIT)Smart(x)x

PistrueinamodelmiffPistruewithxbeingsomepossibleobjectinthemodelRoughlyspeaking,equivalenttothedisjunctionofinstantiationsofP At(KingJohn,HIT)Smart(KingJohn) At(Richard,HIT)Smart(Richard) At(HIT,HIT)Smart(HIT)...Existentialquantification<vaAnothercommonmistaketoavoidTypically,isthemainconnectivewithCommonmistake:usingasthemainconnectivewith:xAt(x,HIT)Smart(x) istrueifthereisanyonewhoisnotatHIT!AnothercommonmistaketoavoiPropertiesofquantifiersxyisthesameasy

xxyisthesameasy

x

xyisnotthesameasy

xxyLoves(x,y)“Thereisapersonwholoveseveryoneintheworld”y

xLoves(x,y)“Everyoneintheworldislovedbyatleastoneperson”Quantifierduality:eachcanbeexpressedusingtheotherxLikes(x,IceCream) xLikes(x,IceCream)xLikes(x,Broccoli) x

Likes(x,Broccoli)PropertiesofquantifiersxyEqualityterm1=term2

istrueunderagiveninterpretationifandonlyifterm1

andterm2

refertothesameobjectE.g.,definitionofSiblingintermsofParent:x,y

Sibling(x,y)[(x=y)

m,f(m=f)Parent(m,x)Parent(f,x)Parent(m,y)Parent(f,y)]Equalityterm1=term2istrueUsingFOLThekinshipdomain:Brothersaresiblingsx,yBrother(x,y)

Sibling(x,y)One'smotherisone'sfemaleparentm,cMother(c)=m

(Female(m)

Parent(m,c))“Sibling”issymmetricx,ySibling(x,y)

Sibling(y,x)UsingFOLThekinshipdomain:UsingFOLThesetdomain:sSet(s)(s={})(x,s2Set(s2)s={x|s2})x,s{x|s}={}x,sxss={x|s}x,sxs[y,s2}(s={y|s2}(x=yxs2))]s1,s2s1

s2

(xxs1

xs2)s1,s2(s1=s2)(s1

s2

s2

s1)x,s1,s2x(s1

s2)(xs1

xs2)x,s1,s2x(s1

s2)(xs1

xs2)UsingFOLThesetdomain:InteractingwithFOLKBsSupposeawumpus-worldagentisusinganFOLKBandperceivesasmellandabreeze(butnoglitter)att=5:Tell(KB,Percept([Smell,Breeze,None],5))Ask(KB,aBestAction(a,5))I.e.,doestheKBentailsomebestactionatt=5?Answer:Yes,{a/Shoot} ←substitution(bindinglist)GivenasentenceSandasubstitutionσ,SσdenotestheresultofpluggingσintoS;e.g.,S=Smarter(x,y)σ={x/Hillary,y/Bill}Sσ=Smarter(Hillary,Bill)Ask(KB,S)returnssome/allσsuchthatKB╞σ

InteractingwithFOLKBsSupposKnowledgebaseforthewumpusworldPerceptiont,s,bPercept([s,b,Glitter],t)Glitter(t)ReflextGlitter(t)BestAction(Grab,t)KnowledgebaseforthewumpusDeducinghiddenpropertiesx,y,a,bAdjacent([x,y],[a,b])

[a,b]{[x+1,y],[x-1,y],[x,y+1],[x,y-1]}Propertiesofsquares:s,tAt(Agent,s,t)Breeze(t)Breezy(s)Squaresarebreezynearapit:Diagnosticrule---infercausefromeffectsBreezy(s)

rAdjacent(r,s)Pit(r)Causalrule---infereffectfromcauserPit(r)[sAdjacent(r,s)Breezy(s)]Deducinghiddenpropertiesx,yKnowledgeengineeringinFOLIdentifythetaskAssembletherelevantknowledgeDecideonavocabularyofpredicates,functions,andconstantsEncodegeneralknowledgeaboutthedomainEncodeadescriptionofthespecificprobleminstancePosequeriestotheinferenceprocedureandgetanswersDebugtheknowledgebaseKnowledgeengineeringinFOLIdTheelectroniccircuitsdomainOne-bitfulladderTheelectroniccircuitsdomainTheelectroniccircuitsdomainIdentifythetaskDoesthecircuitactuallyaddproperly?(circuitverification)AssembletherelevantknowledgeComposedofwiresandgates;Typesofgates(AND,OR,XOR,NOT)Irrelevant:size,shape,color,costofgatesDecideonavocabularyAlternatives:Type(X1)=XORType(X1,XOR)XOR(X1)TheelectroniccircuitsdomainTheelectroniccircuitsdomainEncodegeneralknowledgeofthedomaint1,t2Connected(t1,t2)Signal(t1)=Signal(t2)tSignal(t)=1Signal(t)=01≠0t1,t2Connected(t1,t2)Connected(t2,t1)gType(g)=ORSignal(Out(1,g))=1

nSignal(In(n,g))=1gType(g)=ANDSignal(Out(1,g))=0

nSignal(In(n,g))=0gType(g)=XORSignal(Out(1,g))=1Signal(In(1,g))≠Signal(In(2,g))gType(g)=NOTSignal(Out(1,g))≠Signal(In(1,g))TheelectroniccircuitsdomainTheelectroniccircuitsdomainEncodethespecificprobleminstanceType(X1)=XOR Type(X2)=XORType(A1)=AND Type(A2)=ANDType(O1)=ORConnected(Out(1,X1),In(1,X2)) Connected(In(1,C1),In(1,X1))Connected(Out(1,X1),In(2,A2)) Connected(In(1,C1),In(1,A1))Connected(Out(1,A2),In(1,O1)) Connected(In(2,C1),In(2,X1))Connected(Out(1,A1),In(2,O1)) Connected(In(2,C1),In(2,A1))Connected(Out(1,X2),Out(1,C1)) Connected(In(3,C1),In(2,X2))Connected(Out(1,O1),Out(2,C1)) Connected(In(3,C1),In(1,A2))TheelectroniccircuitsdomainTheelectroniccircuitsdomainPosequeriestotheinferenceprocedureWhatarethepossiblesetsofvaluesofalltheterminalsfortheaddercircuit? i1,i2,i3,o1,o2Signal(In(1,C1))=i1

Signal(In(2,C1))=i2

Signal(In(3,C1))=i3

Signal(Out(1,C1))=o1

Signal(Out(2,C1))=o2DebugtheknowledgebaseMayhaveomittedassertionslike1≠0TheelectroniccircuitsdomainSummaryFirst-orderlogic:objectsandrelationsaresemanticprimitivessyntax:constants,functions,predicates,equality,quantifiersIncreasedexpressivepower:sufficienttodefinewumpusworldSummaryFirst-orderlogic:AssignmentsEx8.3,8.15AssignmentsEx8.3,8.15X.Firstorderlogic(FOL)

Autumn2012Instructor:WangXiaolongHarbinInstituteofTechnology,ShenzhenGraduateSchoolIntelligentComputationResearchCenter(HITSGSICRC)X.Firstorderlogic(FOL)AOutlineWhyFOL?SyntaxandsemanticsofFOLUsingFOLWumpusworldinFOLKnowledgeengineeringinFOLOutlineWhyFOL?ProsandconsofpropositionallogicPropositionallogicisdeclarativePropositionallogicallowspartial/disjunctive/negatedinformation(unlikemostdatastructuresanddatabases)Propositionallogiciscompositional:meaningofB1,1

P1,2isderivedfrommeaningofB1,1andofP1,2Meaninginpropositionallogiciscontext-independent(unlikenaturallanguage,wheremeaningdependsoncontext)Propositionallogichasverylimitedexpressivepower(unlikenaturallanguage)E.g.,cannotsay"pitscausebreezesinadjacentsquares“exceptbywritingonesentenceforeachsquareProsandconsofpropositionalFirst-orderlogicWhereaspropositionallogicassumestheworldcontainsfactsFirst-orderlogic(likenaturallanguage)assumesacarcontainsObjects:people,houses,numbers,colors,baseballgames,wars,…Relations:red,round,prime,brotherof,biggerthan,partof,comesbetween,…Functions:fatherof,bestfriend,onemorethan,plus,…First-orderlogicWhereaspropoExamples:“Oneplustwoequalsthree” Objects: Relations: Properties: Functions:“SquaresneighboringtheWumpusaresmelly” Objects: Relations: Properties: Functions:Examples:“OneplustwoequalsExamples:“Oneplustwoequalsthree” Objects: one,two,three,oneplustwo Relations: equals Properties: -- Functions: plus(“oneplustwo”isthenameoftheobject obtainedbyapplyingfunctionplustooneandtwo; threeisanothernameforthisobject)“SquaresneighboringtheWumpusaresmelly” Objects: Wumpus,square Relations: neighboring Properties: smelly Functions: --Examples:“OneplustwoequalsSemanticsthereisacorrespondencebetweenfunctions,whichreturnvaluespredicates,whicharetrueorfalseFunction:father_of(Mary)=BillPredicate:father_of(Mary,Bill)SemanticsthereisacorrespondSyntaxofFOL:BasicelementsConstants KingJohn,2,HIT,...Predicates Brother,>,...Functions Sqrt,LeftLegOf,...Variables x,y,a,b,...Connectives ,,,,Equality =Quantifiers ,

SyntaxofFOL:BasicelementsCAtomicsentencesAtomicsentence= predicate(term1,...,termn) orterm1=term2Term = function(term1,...,termn) orconstantorvariable

E.g.,Brother(KingJohn,RichardTheLionheart)>(Length(LeftLegOf(Richard)),Length(LeftLegOf(KingJohn)))AtomicsentencesAtomicsentencComplexsentencesComplexsentencesaremadefromatomicsentencesusingconnectivesS,S1

S2,S1S2,S1

S2,S1

S2,E.g.Sibling(KingJohn,Richard)Sibling(Richard,KingJohn)

>(1,2)≤(1,2)>(1,2)

>(1,2)ComplexsentencesComplexsenteTruthinfirst-orderlogicSentencesaretruewithrespecttoamodelandaninterpretationModelcontainsobjects(domain

elements)andrelationsamongthemInterpretationspecifiesreferentsforconstant

symbols

→

objectspredicate

symbols → relationsfunction

symbols → functionalrelationsAnatomicsentencepredicate(term1,...,termn)istrue ifftheobjectsreferredtobyterm1,...,termn areintherelationreferredtobypredicateTruthinfirst-orderlogicSentModelsforFOL:ExampleModelsforFOL:ExampleUniversalquantification<variables><sentence>EveryoneatHITissmart:xAt(x,HIT)Smart(x)xPistrueinamodelmiffPistruewithxbeingeachpossibleobjectinthemodelRoughlyspeaking,equivalenttotheconjunctionofinstantiationsofP At(KingJohn,HIT)Smart(KingJohn) At(Richard,HIT)Smart(Richard) At(HIT,HIT)Smart(HIT) ...Universalquantification<variAcommonmistaketoavoidTypically,isthemainconnectivewithCommonmistake:usingasthemainconnectivewith:xAt(x,HIT)Smart(x)means“EveryoneisatHITandeveryoneissmart”AcommonmistaketoavoidTypicExistentialquantification<variables><sentence>SomeoneatHITissmart:xAt(x,HIT)Smart(x)x

PistrueinamodelmiffPistruewithxbeingsomepossibleobjectinthemodelRoughlyspeaking,equivalenttothedisjunctionofinstantiationsofP At(KingJohn,HIT)Smart(KingJohn) At(Richard,HIT)Smart(Richard) At(HIT,HIT)Smart(HIT)...Existentialquantification<vaAnothercommonmistaketoavoidTypically,isthemainconnectivewithCommonmistake:usingasthemainconnectivewith:xAt(x,HIT)Smart(x) istrueifthereisanyonewhoisnotatHIT!AnothercommonmistaketoavoiPropertiesofquantifiersxyisthesameasy

xxyisthesameasy

x

xyisnotthesameasy

xxyLoves(x,y)“Thereisapersonwholoveseveryoneintheworld”y

xLoves(x,y)“Everyoneintheworldislovedbyatleastoneperson”Quantifierduality:eachcanbeexpressedusingtheotherxLikes(x,IceCream) xLikes(x,IceCream)xLikes(x,Broccoli) x

Likes(x,Broccoli)PropertiesofquantifiersxyEqualityterm1=term2

istrueunderagiveninterpretationifandonlyifterm1

andterm2

refertothesameobjectE.g.,definitionofSiblingintermsofParent:x,y

Sibling(x,y)[(x=y)

m,f(m=f)Parent(m,x)Parent(f,x)Parent(m,y)Parent(f,y)]Equalityterm1=term2istrueUsingFOLThekinshipdomain:Brothersaresiblingsx,yBrother(x,y)

Sibling(x,y)One'smotherisone'sfemaleparentm,cMother(c)=m

(Female(m)

Parent(m,c))“Sibling”issymmetricx,ySibling(x,y)

Sibling(y,x)UsingFOLThekinshipdomain:UsingFOLThesetdomain:sSet(s)(s={})(x,s2Set(s2)s={x|s2})x,s{x|s}={}x,sxss={x|s}x,sxs[y,s2}(s={y|s2}(x=yxs2))]s1,s2s1

s2

(xxs1

xs2)s1,s2(s1=s2)(s1

s2

s2

s1)x,s1,s2x(s1

s2)(xs1

xs2)x,s1,s2x(s1

s2)(xs1

xs2)UsingFOLThesetdomain:InteractingwithFOLKBsSupposeawumpus-worldagentisusinganFOLKBandperceivesasmellandabreeze(butnoglitter)att=5:Tell(KB,Percept([Smell,Breeze,None],5))Ask(KB,aBestAction(a,5))I.e.,doestheKBentailsomebestactionatt=5?Answer:Yes,{a/Shoot} ←substitution(bindinglist)GivenasentenceSandasubstitutionσ,SσdenotestheresultofpluggingσintoS;e.g.,S=Smarter(x,y)σ={x/Hillary,y/Bill}Sσ=Smarter(Hillary,Bill)Ask(KB,S)returnssome/allσsuchthatKB╞σ

InteractingwithFOLKBsSupposKnowledgebaseforthewumpusworldPerceptiont,s,bPercept([s,b,Glitter],t)Glitter(t)ReflextGlitter(t)BestAction(Grab,t)KnowledgebaseforthewumpusDeducinghiddenpropertiesx,y,a,bAdjacent([x,y],[a,b])

[a,b]{[x+1,y],[x-1,y],[x,y+1],[x,y-1]}Propertiesofsquares:s,tAt(Agent,s,t)Breeze(t)Breezy(s)Squaresarebreezynearapit:Diagnosticrule---infercausefromeffectsBreezy(s)

rAdjacent(r,s)Pit(r)Causalrule---infereffectfromcauserPit(r)[sAdjacent(r,s)Breezy(s)]Deducinghiddenpropertiesx,yKnowledgeengineeringinFOLIdentifythetaskAssembletherelevantknowledgeDecideonavocabularyofpredicates,functions,andconstantsEncodegeneralknowledgeaboutthedomainEncodeadescriptionofthespecificprobleminstancePosequeriestotheinferenceprocedureandgetanswersDebugtheknowledgebaseKnowledgeengineeringinFOLIdTheelectroniccircuitsdomainOne-bitfulladderTheelectroniccircuitsdomainTheelectroniccircuitsdomainIdentifythetaskDoesthecircuitactuallyaddproperly?(circuitverification)Assembletherelevantkn