First Order Logic resolution

First Order Logic resolution

1. InferenceinFirst-OrderLogic
PhilippKoehn
16March2017
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

2. 1
ABriefHistoryofReasoning
450B.C.Stoics
322B.C.Aristotle
1565
1847
1879
1922
1930 ¨odel §completealgorithmforFOL
1930
1931 ¨odel §completealgorithmforarithmetic
1960
1965
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

3. 2
TheStorySoFar
YPropositionallogic
YSubsetofprepositionallogic: hornclauses
YInferencealgorithms
–forwardchaining
–backwardchaining
–resolution(forfullprepositionallogic)
YFirstorderlogic(FOL)
–variables
–functions
–quantiers
–etc.
YToday: inferenceforrstorderlogic
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

4. 3
Outline
YReducingrst-orderinferencetopropositionalinference
YUnication
YGeneralizedModusPonens
YForwardandbackwardchaining
YLogicprogramming
YResolution
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

5. 4
reductionto
prepositionalinference
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

6. 5
UniversalInstantiation
YEveryinstantiationofauniversallyquantiedsentenceisentailedbyit:
¦v
SUBSTˆ˜v~g;
foranyvariablevandgroundtermg
YE.g.,¦x Kingˆ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

Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

7. 6
ExistentialInstantiation
YForanysentence,variablev,andconstantsymbolk
thatdoesnotappearelsewhereintheknowledgebase:
§v
SUBSTˆ˜v~k;
YE.g.,§x Crownˆx,OnHeadˆx;Johnyields
CrownˆC1,OnHeadˆC1;John
providedC1isanewconstantsymbol,calleda
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

8. 7
Instantiation
YUniversalInstantiation
–canbeappliedseveraltimestoaddnewsentences
–thenewKBislogicallyequivalenttotheold
YExistentialInstantiation
–canbeappliedoncetoreplacetheexistentialsentence
–thenewKBisnotequivalenttotheold
–butissatisableifftheoldKBwassatisable
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

9. 8
ReductiontoPropositionalInference
YSupposetheKBcontainsjustthefollowing:
¦x Kingˆx,GreedyˆxÔEvilˆx
KingˆJohn
GreedyˆJohn
BrotherˆRichard;John
YInstantiatingtheuniversalsentenceinall possibleways,wehave
KingˆJohn,GreedyˆJohnÔEvilˆJohn
KingˆRichard,GreedyˆRichardÔEvilˆRichard
KingˆJohn
GreedyˆJohn
BrotherˆRichard;John
YThenewKBis: propositionsymbolsare
KingˆJohn; GreedyˆJohn; EvilˆJohn;BrotherˆRichard;John;etc.
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

10. 9
ReductiontoPropositionalInference
YClaim: agroundsentence
‡
isentailedbynewKBiffentailedbyoriginalKB
YClaim: everyFOLKBcanbepropositionalizedsoastopreserveentailment
YIdea: propositionalizeKBandquery,applyresolution,returnresult
YProblem: withfunctionsymbols,thereareinnitelymanygroundterms,
e.g.,FatherˆFatherˆFatherˆJohn
YTheorem: Herbrand(1930). IfasentenceisentailedbyanFOLKB,
itisentailedbyanitesubsetofthepropositionalKB
YIdea: Forn=0toªdo
createapropositionalKBbyinstantiatingwithdepth-nterms
seeifisentailedbythisKB
YProblem: worksifisentailed,loopsifisnotentailedYTheorem: Turing(1936),Church(1936),entailmentinFOLis
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

11. 10
PracticalProblemswithPropositionalization
YPropositionalizationseemstogeneratelotsofirrelevantsentences.
YE.g.,from ¦x Kingˆx,GreedyˆxÔEvilˆx
KingˆJohn
¦y Greedyˆy
BrotherˆRichard;John
itseemsobviousthatEvilˆJohn,butpropositionalizationproduceslotsoffacts
suchasGreedyˆRichardthatareirrelevant
YWithp-arypredicatesandnconstants,therearepn
k
instantiations
YWithfunctionsymbols,itgetsnuchmuchworse!
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

12. 11
unication
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

13. 12
Plan
YWehavetheinferencerule
–¦x Kingˆx,GreedyˆxÔEvilˆx
YWehavefactsthat(partially)matchtheprecondition
–KingˆJohn
–¦y Greedyˆy
YWeneedtomatchthemupwithsubstitutions: ˜x~John;y~Johnworks
–unication
–generalizedmodusponens
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

14. 13
Unication
YUNIFYˆ;if
p q
KnowsˆJohn;xKnowsˆJohn;Jane
KnowsˆJohn;xKnowsˆy;Mary
KnowsˆJohn;xKnowsˆy;Motherˆy
KnowsˆJohn;xKnowsˆx;Mary
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

15. 14
Unication
YUNIFYˆ;if
p q
KnowsˆJohn;xKnowsˆJohn;Jane˜x~Jane
KnowsˆJohn;xKnowsˆy;Mary
KnowsˆJohn;xKnowsˆy;Motherˆy
KnowsˆJohn;xKnowsˆx;Mary
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

16. 15
Unication
YUNIFYˆ;if
p q
KnowsˆJohn;xKnowsˆJohn;Jane˜x~Jane
KnowsˆJohn;xKnowsˆy;Mary ˜x~Mary;y~John
KnowsˆJohn;xKnowsˆy;Motherˆy
KnowsˆJohn;xKnowsˆx;Mary
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

17. 16
Unication
YUNIFYˆ;if
p q
KnowsˆJohn;xKnowsˆJohn;Jane˜x~Jane
KnowsˆJohn;xKnowsˆy;Mary ˜x~Mary;y~John
KnowsˆJohn;xKnowsˆy;Motherˆy˜y~John;x~MotherˆJohn
KnowsˆJohn;xKnowsˆx;Mary
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

18. 17
Unication
YUNIFYˆ;if
p q
KnowsˆJohn;xKnowsˆJohn;Jane˜x~Jane
KnowsˆJohn;xKnowsˆy;Mary ˜x~Mary;y~John
KnowsˆJohn;xKnowsˆy;Motherˆy˜y~John;x~MotherˆJohn
KnowsˆJohn;xKnowsˆx;Mary fail
YStandardizingapart Knowsˆz17;Mary
KnowsˆJohn;xKnowsˆz17;Mary ˜z17~John;x~Mary
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

19. 18
generalizedmodusponens
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

20. 19
GeneralizedModusPonens
YGeneralizedmodusponensusedwithKBof denite clauses
(exactlyonepositiveliteral)
YAllvariablesassumeduniversallyquantied
p1
œ
; p2
œ
; :::; pn
œ
;ˆp1,p2,:::,pnq
q
wherepi
œ
piforalli
YRule: Kingˆx,GreedyˆxÔEvilˆx
YPreconditionofrule: p1isKingˆx p2isGreedyˆx
YImplication: qisEvilˆx
YFacts: p1
œ
isKingˆJohnp2
œ
isGreedyˆyYSubstitution: is˜x~John;y~John
Resultofmodusponens:qisEvilˆJohn
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

21. 20
forwardchaining
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

22. 21
ExampleKnowledge
YThelawsaysthatitisacrimeforanAmericantosellweaponstohostilenations.
The country Nono, an enemy of America, has some missiles, and all of its
missilesweresoldtoitbyColonelWest,whoisAmerican.
YProvethatCol.Westisacriminal
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

23. 22
ExampleKnowledgeBase
Y:::itisacrimeforanAmericantosellweaponstohostilenations:
Americanˆx,Weaponˆy,Sellsˆx;y;z,HostileˆzÔCriminalˆx
YNono:::hassomemissiles
,i.e.,§xOwnsˆNono;x,Missileˆx:
OwnsˆNono;M1andMissileˆM1
Y:::allofitsmissilesweresoldtoitbyColonelWest
¦x Missileˆx,OwnsˆNono;xÔSellsˆWest;x;Nono
YMissilesareweapons:
MissileˆxWeaponˆx
YAnenemyofAmericacountsas“hostile”:
Enemyˆx;AmericaÔHostileˆx
YWest,whoisAmerican:::
AmericanˆWest
YThecountryNono,anenemyofAmerica :::
EnemyˆNono;America
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

24. 23
ForwardChainingProof
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

25. 24
ForwardChainingProof
(Note:¦x Missileˆx,OwnsˆNono;xÔSellsˆWest;x;Nono)
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

26. 25
ForwardChainingProof
(Note:Americanˆx,Weaponˆy,Sellsˆx;y;z,HostileˆzÔCriminalˆx)
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

27. 26
PropertiesofForwardChaining
YSoundandcompleteforrst-orderdeniteclauses
(proofsimilartopropositionalproof)
YDatalog(1977)=rst-orderdeniteclauses+nofunctions(e.g.,crimeKB)
ForwardchainingterminatesforDataloginpolyiterations: atmostpn
k
literals
YMaynotterminateingeneralifisnotentailed
YThisisunavoidable: entailmentwithdeniteclausesissemidecidable
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

28. 27
EfciencyofForwardChaining
YSimpleobservation: noneedtomatcharuleoniterationk
ifapremisewasn'taddedoniterationk1
Ômatcheachrulewhosepremisecontainsanewlyaddedliteral
YMatchingitselfcanbeexpensive
YDatabaseindexing Oˆ1retrievalofknownfacts
e.g.,queryMissileˆxretrievesMissileˆM1
YMatchingconjunctivepremisesagainstknownfactsisNP-hard
YForwardchainingiswidelyusedin
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

29. 28
HardMatchingExample
Diffˆ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
YColorableˆisinferredifftheconstraintsatisfactionproblemhasasolution
YCSPsinclude3SATasaspecialcase,hencematchingisNP-hard
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

30. 29
ForwardChainingAlgorithm
functionFOL-FC-ASK(KB,)returnsasubstitutionorfalse
repeat untilnewisempty
newg
for eachsentencerinKBdo
ˆp1,:::,pnÔqSTANDARDIZE-APART(r)
for eachsuchthatˆp1,:::,pnˆp
œ
1
,:::,p
œ
n
forsomep
œ
1
;:::;p
œ
ninKB
q
œ
SUBST(,q)
ifq
œ
isnotarenamingofasentencealreadyinKBornewthen do
addq
œ
tonew
UNIFY(q
œ
,)
ifisnotfailthen return
addnewtoKB
returnfalse
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

31. 30
backwardchaining
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

32. 31
BackwardChaining
YStartwithquery
YCheckifitcanbederivedbygivenrulesandfacts
–applyrulesthatinferthequery
–recurseoverpre-conditions
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

33. 32
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

34. 33
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

35. 34
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

36. 35
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

37. 36
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

38. 37
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

39. 38
BackwardChainingExample
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

40. 39
PropertiesofBackwardChaining
YDepth-rstrecursiveproofsearch: spaceislinearinsizeofproof
YIncompleteduetoinniteloops
Ôxbycheckingcurrentgoalagainsteverygoalonstack
YInefcientduetorepeatedsubgoals(bothsuccessandfailure)
Ôxusingcachingofpreviousresults(extraspace!)
YWidelyused(withoutimprovements!) for
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

41. 40
BackwardChainingAlgorithm
functionFOL-BC-ASK(KB,goals,)returnsasetofsubstitutions
inputs:KB,aknowledgebase
goals,alistofconjunctsformingaquery(alreadyapplied)
,thecurrentsubstitution,initiallytheemptysubstitutiong
local variables:answers,asetofsubstitutions,initiallyempty
ifgoalsisemptythen return˜
q
œ
SUBST(,FIRST(goals))
for eachsentencerinKB
whereSTANDARDIZE-APART(r)=ˆp1,:::,pnq
and
œ
UNIFY(q,q
œ
)succeeds
newgoalsp1;:::;pnSREST(goals)
answersFOL-BC-ASK(KB,newgoals,COMPOSE(
œ
,))8answers
returnanswers
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

42. 41
logicprogramming
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

43. 42
LogicProgramming
YSoundbite: computationasinferenceonlogicalKBs
Logicprogramming
1. Identifyproblem Identifyproblem
2. Assembleinformation Assembleinformation3. Teabreak Figureoutsolution4. EncodeinformationinKB Programsolution5. Encodeprobleminstanceasfacts Encodeprobleminstanceasdata6. Askqueries Applyprogramtodata7. Findfalsefacts Debugproceduralerrors
YShouldbeeasiertodebugCapitalˆNewYork;USthanxx2!
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

44. 43
Prolog
YBasis: backwardchainingwithHornclauses+bells&whistles
YWidelyusedinEurope,Japan(basisof5thGenerationproject)
YCompilationtechniquesapproachingabillionlogicalinferencespersecond
YProgram=setofclauses=head :- literal1,:::literaln.
criminal(X) :- american(X), weapon(Y), sells(X,Y,Z), hostile(Z).
missile(M1).
owns(Nono,M1).
sells(West,X,Nono) :- missile(X), owns(Nono,X).
weapon(X) :- missile(X).
hostile(X) :- enemy(X,America).
American(West).
Enemy(Nono,America).
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

45. 44
PrologSystems
YEfcientunicationby
YEfcientretrievalofmatchingclausesbydirectlinking
YDepth-rst,left-to-rightbackwardchaining
YBuilt-inpredicatesforarithmeticetc.,e.g.,X is Y*Z+3
YClosed-worldassumption(“negationasfailure”)
e.g.,givenalive(X) :- not dead(X).
alive(joe)succeedsifdead(joe)fails
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

46. 45
resolution
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

47. 46
Resolution:BriefSummary
YFullrst-orderversion:
`1--`k; m 1--mn
ˆ`1--`i1-`i1--`k-m1--mj1-mj1--mn
whereUNIFYˆ`i; mj.
YForexample,
Richˆx-Unhappyˆx
RichˆKen
UnhappyˆKen
with˜x~Ken
YApplyresolutionstepstoCNFˆKB, ;completeforFOL
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

48. 47
ConversiontoCNF
Everyonewholovesallanimalsislovedbysomeone:
¦x¦y AnimalˆyÔLovesˆx;yÔ§y Lovesˆy;x
1. Eliminatebiconditionalsandimplications
¦x ¦y Animalˆy-Lovesˆx;y-§y Lovesˆy;x
2. Move inwards: ¦x;p§x p, §x;p¦x p:
¦x§y ˆ Animalˆy-Lovesˆx;y-§y Lovesˆy;x
¦x§y Animalˆy, Lovesˆx;y-§y Lovesˆy;x
¦x§y Animalˆy, Lovesˆx;y-§y Lovesˆy;x
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

49. 48
ConversiontoCNF
3. Standardizevariables: eachquantiershoulduseadifferentone
¦x§y Animalˆy, Lovesˆx;y-§z Lovesˆz;x
4. Skolemize: amoregeneralformofexistentialinstantiation.
Eachexistentialvariableisreplacedbya
oftheenclosinguniversallyquantiedvariables:
¦xAnimalˆFˆx, Lovesˆx;Fˆx-LovesˆGˆx;x
5. Dropuniversalquantiers:
AnimalˆFˆx, Lovesˆx;Fˆx-LovesˆGˆx;x
6. Distribute,over-:
AnimalˆFˆx-LovesˆGˆx;x, Lovesˆx;Fˆx-LovesˆGˆx;x
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

50. 49
OurPreviousExample
YRules
–Americanˆx,Weaponˆy,Sellsˆx;y;z,HostileˆzÔCriminalˆx
–MissileˆM1andOwnsˆNono;M1
–¦x Missileˆx,OwnsˆNono;xÔSellsˆWest;x;Nono
–MissileˆxWeaponˆx
–Enemyˆx;AmericaÔHostileˆx
–AmericanˆWest
–EnemyˆNono;America
YConvertedtoCNF
– Americanˆx- Weaponˆy- Sellsˆx;y;z- Hostileˆz-Criminalˆx
–MissileˆM1andOwnsˆNono;M1
– Missileˆx- OwnsˆNono;x-SellsˆWest;x;Nono
– Missileˆx-Weaponˆx
– Enemyˆx;America-Hostileˆx
–AmericanˆWest
–EnemyˆNono;America
YQuery: CriminalˆWest
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017

51. 50
ResolutionProof
Philipp Koehn Articial Intelligence: Inference in First-Order Logic 16 March 2017