19-Inferencia_em_LPO

Prévia do material em texto

INFERÊNCIA	
  EM	
  LPO	
  
	
  
	
  
Raciocínio	
  com	
  variáveis	
  
¨  Uma	
   	
  de	
  um	
  átomo	
  ou	
  uma	
  cláusula	
  é	
  obAda	
  
subsAtuindo-­‐se	
  uniformemente	
  termos	
  para	
  variáveis.	
  
¨  Uma	
   	
  é	
  um	
  conjunto	
  de	
  finito	
  de	
  forma	
  {V1/t1,	
  ...,	
  
Vn/tn},	
  onde	
  cada	
  Vi	
  é	
  uma	
  variável	
  disAnta	
  e	
  cada	
  ti	
  é	
  um	
  
termo.	
  
¨  A	
   	
  de	
  uma	
  subsAtuição	
  σ	
  =	
  {V1/t1,	
  ...,	
  Vn/tn}	
  para	
  um	
  
átomo	
  ou	
  cláusula	
  e,	
  escrito	
  eσ,	
  é	
  a	
  instância	
  de	
  e	
  com	
  todas	
  
as	
  ocorrências	
  do	
  Vi	
  subsAtuídas	
  por	
  ti.	
  
Exemplos	
  de	
  aplicações	
  
¨  Os	
  exemplos	
  abaixo	
  são	
  subsAtuições:	
  
	
  σ1	
  =	
  {X/A,Y/b,Z/C,D/e}	
  
	
  σ2	
  =	
  {A/X,Y/b,C/Z,D/e}	
  
	
  σ3	
  =	
  {A/V,X/V,Y/b,C/W,Z/W,D/e}	
  
	
  
¨  Abaixo	
  temos	
  algumas	
  aplicações:	
  
	
  p(A,b,C,D)σ1	
  =	
  p(A,b,C,e)	
  
	
  p(X,Y,Z,e)σ1	
  =	
  p(A,b,C,e)	
  
	
  p(A,b,C,D)σ2	
  =	
  p(X,b,Z,e)	
  
	
  p(X,Y,Z,e)σ2	
  =	
  p(X,b,Z,e)	
  
	
  p(A,b,C,D)σ3	
  =	
  p(V,b,W,e)	
  
	
  p(X,Y,Z,e)σ3	
  =	
  p(V,b,W,e)	
  
Inferência	
  em	
  LP	
  X	
  LPO	
  
4 
¨  Uma	
  ideia	
  básica	
  é	
  converter	
  a	
  BC	
  em	
  LPO	
  para	
  uma	
  BC	
  em	
  LP	
  e	
  
aplicar	
  inferência	
  proposicional.	
  
¨  A	
  regra	
  de	
   (UI)	
  afirma	
  que,	
  em	
  com	
  uma	
  
sentença	
  universalmente	
  quanAficada,	
  podemos	
  deduzir	
  qualquer	
  
sentença	
  obAda	
  pela	
  subsAtuição	
  de	
  um	
  termo	
  básico	
  (sem	
  
variáveis)	
  para	
  uma	
  variável.	
  
¨  Exemplo:	
  	
  
¤  Da	
  sentença	
  ∀X rei(X) ٨۸ guloso(X) => perverso(X). 
¤  Podemos	
  derivar:	
  
n  rei(joão) ٨۸ guloso(joão) => perverso(joão). 
n  rei(ricardo) ٨۸ guloso(ricardo) => perverso(ricardo). 
n  rei(pai(joão)) ٨۸ guloso(pai(joão)) => perverso(pai(joão)). 
Instanciação	
  Universal	
  
5 
¨  As	
  três	
  sentenças	
  anteriores	
  foram	
  obAdas	
  pelas	
  
subsAtuições	
  da	
  variável	
  x	
  por	
  um	
  termo	
  básico	
  da	
  BC:	
  
¤  {X/joão}, {X/ricardo}, {X/pai(joão)} 
¨  Seja	
  SUBST(θ,	
  α)	
  o	
  resultado	
  da	
  subsAtuição	
  θ	
  à	
  sentença	
  α.	
  
Então	
  a	
  regra	
  de	
  instanciação	
  universal	
  é	
  escrita	
  como:	
  
	
  ∀V	
  α 	
   	
   	
   	
  onde	
  V	
  é	
  uma	
  variável	
  e	
  
	
  SUBST({V/g},	
  α) 	
   	
  	
  g	
  é	
  um	
  termo	
  básico	
  
Instanciação	
  Existencial	
  
6 
¨  A	
  regra	
  de	
   é	
  um	
  pouco	
  mais	
  complicada.	
  
¨  Para	
  qualquer	
  sentença	
  existencialmente	
  quanAficada	
  α,	
  
variável	
  V,	
  e	
  símbolo	
  de	
  constante	
  k	
  que	
  não	
  apareça	
  na	
  BC:	
  
	
  ∃V	
  α 	
   	
   	
  onde	
  V	
  é	
  uma	
  variável	
  e	
  k	
  é	
  uma	
  
	
  SUBST({V/k},	
  g) 	
  constante	
  que	
  não	
  aparece	
  em	
  BC	
  
¨  Exemplo:	
  	
  
¤  Da	
  sentença	
  ∃X coroa(X) ٨۸ naCabeça(X,joão).	
  
¤  Podemos	
  derivar	
  a	
  sentença:	
  
n  coroa(c1) ٨۸ naCabeça(c1,joão).	
  Desde	
  que	
  c1	
  não	
  apareça	
  em	
  
outro	
  lugar	
  na	
  BC.	
  
Instanciação	
  Existencial	
  
7 
¨  A	
  sentença	
  existencial	
  afirma	
  que	
  existe	
  algum	
  objeto	
  que	
  saAsfaz	
  
a	
  uma	
  condição.	
  
¨  O	
  processo	
  de	
  instanciação	
  apenas	
  dá	
  um	
  nome	
  a	
  este	
  objeto.	
  
¨  Este	
  nome	
  (a	
  constante	
  uAlizada)	
  é	
  chamada	
  de	
  
,	
  porque	
  a	
  instanciação	
  do	
  existencial	
  é	
  um	
  caso	
  especial	
  de	
  
um	
  processo	
  chamado	
  de	
   .	
  
¨  Em	
  termos	
  de	
  inferência	
  a	
  sentença	
  existencial	
  
,	
  e	
  depois	
  a	
  sentença	
  pode	
  ser	
  descartada.	
  
¤  Diferente	
  da	
  sentença	
  universal	
  que	
  pode	
  ser	
  aplicada	
  várias	
  vezes	
  com	
  
subsAtuições	
  diferentes.	
  
Redução	
  à	
  inferência	
  proposicional	
  
8 
¨  As	
  sentenças	
  existencialmente	
  quanAficadas	
  podem	
  ser	
  subsAtuídas	
  por	
  
	
   .	
  
¨  As	
  sentenças	
  universalmente	
  quanAficadas	
  podem	
  ser	
  subsAtuídas	
  por	
  
.	
  
¤  Considere	
  a	
  seguinte	
  BC:	
  
n  ∀X rei(x) ٨۸ guloso(X) => perverso(X). 
n  rei(joão). 
n  guloso(joão). 
n  irmão(ricardo, joão). 
¤  Aplicando	
  UI	
  à	
  primeira	
  sentença,	
  obtemos:	
  
n  rei(joão) ٨۸ guloso(joão) => perverso(joão). 
n  rei(ricardo) ٨۸ guloso(ricardo) => perverso(ricardo). 
n  e	
  podemos	
  descartar	
  a	
  sentença	
  universalmente	
  quanAficada.	
  
Redução	
  à	
  inferência	
  proposicional	
  
9 
¨  Agora	
  a	
  BC	
  é	
  essencialmente	
  proposicional	
  se	
  visualizarmos	
  
as	
  sentenças	
  atômicas	
  básicas	
  como	
  símbolos	
  proposicionais:	
  
¤  rei(joão) ٨۸ guloso(joão) => perverso(joão). 
¤  rei(ricardo) ٨۸ guloso(ricardo) => perverso(ricardo). 
¤  rei(joão). 
¤  guloso(joão). 
¤  irmão(ricardo,joão). 
¨  Esta	
  técnica	
  é	
  chamada	
  de	
   e	
  pode	
  se	
  
tornar	
  totalmente	
  geral.	
  
¤  Toda	
  BC	
  em	
  LPO	
  e	
  toda	
  consulta	
  pode	
  ser	
  proposicionalizada	
  de	
  forma	
  
que	
  a	
  consequência	
  lógica	
  é	
  preservada.	
  
Redução	
  à	
  inferência	
  proposicional	
  
10 
¨  Porém,	
  o	
  procedimento	
  de	
  decisão	
  para	
  consequência	
  lógica	
  
não	
  é	
  completo.	
  
¨  Se	
  a	
  BC	
  conter	
  um	
  símbolo	
  de	
  função,	
  o	
  conjunto	
  de	
  
subsAtuições	
  possíveis	
  de	
  termos	
  básicos	
  é	
  infinito:	
  
¤  Por	
  exemplo:	
  se	
  a	
  BC	
  contém	
  o	
  símbolo	
  pai,	
  então	
  pai(joão) é	
  um	
  
termo,	
  assim	
  como	
  pai(pai(joão)) e	
  
pai(pai(pai(joão))) e	
  ...	
  também	
  são.	
  
:	
  Se	
  BC|=	
  α	
  na	
  BC	
  em	
  LPO	
  original,	
  
então	
  existe	
  uma	
  prova	
  envolvendo	
  um	
  subconjunto	
  finito	
  da	
  
BC	
  proposicionalizada.	
  
Redução	
  à	
  inferência	
  proposicional	
  
11 
¨  Podemos	
  encontrar	
  o	
  subconjunto	
  do	
  teorema	
  de	
  Herbrand:	
  
¤  Gerando	
  primeiro	
  todas	
  as	
  instanciações	
  com	
  símbolos	
  de	
  constantes,	
  
depois	
  todos	
  os	
  termos	
  de	
  profundidade	
  1,	
  depois	
  de	
  profundidade	
  
2...	
  
¤  Até	
  sermos	
  capazes	
  de	
  construir	
  uma	
  prova	
  proposicional	
  da	
  sentença	
  
que	
  é	
  consequência	
  lógica.	
  
¨  Assim,	
  qualquer	
  sentença	
  que	
   consequência	
  lógica	
  pode	
  ser	
  
provada.	
  Mas	
  não	
  sabemos	
  se	
  ela	
  é	
  consequência	
  lógica	
   	
  a	
  
prova	
  terminar.	
  
¤  O	
  procedimento	
  de	
  prova	
  pode	
  prosseguir	
  gerando	
  termos	
  cada	
  vez	
  
mais	
  profundamente	
  aninhados,	
  mas	
  não	
  sabemos	
  se	
  ele	
  ficou	
  preso	
  
ou	
  se	
  a	
  prova	
  está	
  terminando.	
  
A	
  proposicionalização	
  é	
  ineficiente	
  
12 
¨  Exemplo:	
  Considere	
  a	
  consulta	
  perverso(X)	
  e	
  a	
  BC	
  original	
  
em	
  LPO.	
  
¤  Se	
  considerarmoso	
  conjunto	
  de	
  sentenças	
  da	
  BC	
  original	
  e	
  LPO:	
  
n  ∀X rei(X) ٨۸ guloso(X) => perverso(X). 
n  rei(joão). 
n  guloso(joão). 
¤  A	
  dedução	
  de	
  perverso(joão) é	
  bastante	
  óbvia	
  para	
  nós.	
  
¤  Parece	
  inconveniente	
  gerar	
  sentenças	
  como	
  rei(ricardo) ٨۸ 
guloso(ricardo) => perverso(ricardo) para	
  esta	
  consulta.	
  
¤  Imagine	
  ainda	
  se	
  Avermos	
  muitos	
  outros	
  termos	
  básicos.	
  
Uma	
  regra	
  de	
  inferência	
  para	
  LPO	
  
13 
¨  Para	
  a	
  consulta	
  perverso(X)	
  podemos	
  encontrar	
  algum	
  X	
  tal	
  
que	
  x	
  seja	
  um	
  rei	
  e	
  que	
  X	
  seja	
  guloso,	
  e	
  depois	
  deduzir	
  que	
  X	
  
é	
  perverso.	
  
¨  De	
  modo	
  geral: 	
  	
  
¤  Se	
  houver	
  alguma	
  subsAtuição	
  θ	
  que	
  torne	
  a	
  premissa	
  da	
  implicação	
  
idênAca	
  as	
  sentenças	
  que	
  já	
  estão	
  na	
  BC,	
  podemos	
  afirmar	
  a	
  conclusão	
  
da	
  implicação,	
  depois	
  da	
  aplicação	
  de	
  θ.	
  
n  No	
  exemplo,	
  a	
  subsAtuição	
  {X/joão}	
  alcança	
  este	
  objeAvo.	
  
Uma	
  regra	
  de	
  inferência	
  para	
  LPO	
  
14 
¨  Vamos	
  supor	
  que	
  a	
  sentença	
  guloso(joão),	
  seja	
  subsAtuída	
  pela	
  
sentença	
  ∀Y	
  guloso(Y).	
  
¨  Ainda	
  podemos	
  concluir	
  perverso(joão)	
  porque	
  João	
  é	
  um	
  rei	
  e	
  	
  é	
  
guloso	
  (porque	
  todo	
  mundo	
  é	
  guloso).	
  
¨  A	
  aplicação	
  da	
  subsAtuição	
  {X/joão,	
  Y/joão}	
  às	
  premissas	
  da	
  
implicação	
  e	
  às	
  sentenças	
  da	
  BC	
  às	
  tornará	
  idênAcas.	
  
:	
  para	
  as	
  sentenças	
  atômicas	
  pi,	
  p'i	
  e	
  
q,	
  onde	
  existe	
  uma	
  subsAtuição	
  θ	
  	
  tal	
  que	
  SUBST(θ,	
  p'i)	
  =	
  SUBST(θ,	
  
pi),	
  para	
  todo	
  i,	
  
	
  p'1,	
  p'2,	
  ...,	
  p'n,	
  (p1	
  ٨	
  p2	
  ٨	
  ...	
  ٨	
  pn	
  =>	
  q)	
  
	
   	
   	
  SUBST(θ,	
  q)	
  
Modus	
  Ponens	
  Generalizado	
  
15 
	
  p'1,	
  p'2,	
  ...,	
  p'n,	
  (p1	
  ٨	
  p2	
  ٨	
  ...	
  ٨	
  pn	
  =>	
  q)	
  
	
   	
   	
  SUBST(θ,	
  q)	
  
	
  
¨  Para	
  o	
  exemplo:	
  
¤  p'1	
  é	
  rei(joão) 	
  p1	
  é	
  rei(X) 	
   	
  {X/joão}	
  
¤  p'2	
  é	
  guloso(Y) 	
  p2	
  é	
  guloso(X) 	
   	
  {X/joão}	
  e	
  {Y/joão}	
  
¤  θ	
  é	
  {X/joão,	
  Y/joão} 	
  q	
  é	
  perverso(X)‏ 
¤  SUBST(θ,	
  q)	
  é	
  perverso(joão)‏ 
Unificação	
  
16 
¨  Regras	
  de	
  inferência	
  como	
  Modus	
  Ponens	
  Generalizado	
  
exigem	
  a	
  descoberta	
  de	
  subsAtuições	
  que	
  façam	
  duas	
  
expressões	
  lógicas	
  diferentes	
  parecerem	
  idênAcas.	
  
¨  Esse	
  processo	
  é	
  chamado	
  de	
   e	
  é	
  um	
  componente	
  
fundamental	
  de	
  todo	
  algoritmo	
  de	
  inferência	
  em	
  LPO.	
  
¨  O	
  algoritmo	
  de	
  unificação	
  recebe	
  duas	
  sentenças	
  e	
  retorna	
  
um	
  unificador	
  para	
  elas,	
  se	
  exisAr	
  algum.	
  
¨  Como	
  exemplo,	
  suponha	
  que	
  temos	
  uma	
  consulta	
  à	
  BC	
  
conhece(joão,	
  X)	
  à	
  quem	
  conhece	
  João?	
  
Unificação	
  
17 
¨  Suponha	
  que	
  a	
  BC	
  dispõe	
  das	
  sentenças:	
  
¤  conhece(joão,	
  jane)	
  
¤  conhece(Y,	
  bill)	
  
¤  conhece(Y,	
  mãe(Y)	
  
¤  conhece(X,	
  elizabeth)	
  
¨  Resultados	
  da	
  Unificação:	
  
¤  UNIFICAR(conhece(joão,	
  X),	
  conhece(joão,	
  jane))	
  =	
  {X/jane}	
  
¤  UNIFICAR(conhece(joão,	
  X),	
  conhece(Y,	
  bill))	
  =	
  {X/bill,	
  Y/joão}	
  
¤  UNIFICAR(conhece(joão,	
  X),	
  conhece(Y,	
  mãe(Y)))	
  =	
  {Y/joão,	
  X/mãe(joão)}	
  
¤  UNIFICAR(conhece(joão,	
  X),	
  conhece(X,	
  elizabeth))	
  =	
  falha	
  
Unificador	
  
¨  A	
  subsAtuição	
  σ	
  é	
  um	
   	
  de	
  e1	
  e	
  e2	
  se	
  e1σ	
  =	
  e2σ.	
  
¨  A	
  subsAtuição	
  σ	
  é	
  o	
   (umg)	
  de	
  e1	
  e	
  e2	
  se	
  
n  σ	
  é	
  um	
  unificador	
  de	
  e1	
  e	
  e2;	
  e	
  
n  se	
  a	
  subsAtuição	
  σ’	
  também	
  unifica	
  e1	
  e	
  e2,	
  então	
  eσ’	
  é	
  
uma	
  instância	
  de	
  eσ	
  para	
  todos	
  os	
  átomos	
  e.	
  
¨  Se	
  dois	
  átomos	
  têm	
  um	
  unificador,	
  eles	
  têm	
  um	
  unificador	
  
mais	
  geral.	
  
Exemplo	
  de	
  Unificação	
  
¨  p(A,b,C,D)	
  e	
  p(X,Y,Z,e)	
  tem	
  unificadores:	
  
	
  σ1	
  =	
  {X/A,Y/b,Z/C,D/e}	
  
	
  σ2	
  =	
  {A/X,Y/b,C/Z,D/e}	
  
	
  σ3	
  =	
  {A/V,X/V,Y/b,C/W,Z/W,D/e}	
  
	
  σ4	
  =	
  {A/a,X/a,Y/b,C/c,Z/c,D/e}	
  
	
  σ5	
  =	
  {X/A,Y/b,Z/A,C/A,D/e}	
  
	
  σ6	
  =	
  {X/A,Y/b,Z/C,D/e,W/a}	
  
	
  
¨  A	
  primeira	
  de	
  três	
  são	
  unificadores	
  mais	
  gerais.	
  
¨  As	
  subsAtuições	
  a	
  seguintes	
  não	
  são	
  unificadoras:	
  
	
  σ7	
  =	
  {Y/b,D/e}	
  
	
  σ8	
  =	
  {X/a,Y/b,Z/c,D/e}	
  
Renomeando	
  variáveis	
  
20 
¨  A	
  unificação:	
  
¤  UNIFICAR(conhece(joão,	
  X),	
  conhece(X,	
  elizatbeth))	
  falha	
  somente	
  
porque	
  X	
  não	
  pode	
  assumir	
  os	
  valores	
  joão	
  e	
  elizabeth	
  ao	
  mesmo	
  
tempo.	
  
¨  Pois	
  a	
  sentença	
  conhece(X,	
  elizabeth)	
  significa	
  que	
  “Todo	
  
mundo	
  conhece	
  elizabeth”	
  –	
  inclusive	
  o	
  joão.	
  
¨  O	
  problema	
  só	
  surge	
  porque	
  as	
  duas	
  sentenças	
  uAlizam	
  o	
  
mesmo	
  nome	
  de	
  variável,	
  X.	
  
¨  Isto	
  pode	
  ser	
  evitado	
  renomeando	
  as	
  variáveis	
  de	
  uma	
  das	
  
duas	
  sentenças	
  –	
   .	
  
Unificador	
  Mais	
  Geral	
  
21 
¨  A	
  unificação:	
  	
  
¤  UNIFICAR(conhece(joão,X),	
  conhece(Y,	
  Z))	
  
¨  Poderia	
  retornar:	
  
¤  {Y/	
  João,	
  X/Z}	
  à	
  conhece(joão,	
  Z)	
  com	
  resultado	
  
¤  {Y/	
  João,	
  X/João,	
  Z/João}	
  -­‐>	
  conhece(joão,	
  joão)‏	
  
¨  O	
  primeiro	
  unificador	
  é	
  mais	
  geral	
  que	
  o	
  segundo,	
  porque	
  
impõe	
  menos	
  restrições	
  sobre	
  os	
  valores	
  das	
  variáveis.	
  
¨  Para	
  todo	
  par	
  de	
  expressões	
  que	
  deve	
  ser	
  unificado,	
  existe	
  
um	
  único	
   ou	
  UMG.	
  
Algoritmo	
  de	
  Unificação	
  
9 INFERENCE INFIRST-ORDER LOGIC
function UNIFY(x , y , θ) returns a substitution to make x and y identical
inputs: x , a variable, constant, list, or compound expression
y , a variable, constant, list, or compound expression
θ, the substitution built up so far (optional, defaults to empty)
if θ = failure then return failure
else if x = y then return θ
else if VARIABLE?(x ) then return UNIFY-VAR(x , y , θ)
else if VARIABLE?(y) then return UNIFY-VAR(y , x , θ)
else if COMPOUND?(x ) and COMPOUND?(y) then
return UNIFY(x .ARGS, y .ARGS, UNIFY(x .OP, y .OP, θ))
else if LIST?(x ) and LIST?(y) then
return UNIFY(x .REST, y .REST, UNIFY(x .FIRST, y .FIRST, θ))
else return failure
function UNIFY-VAR(var , x , θ) returns a substitution
if {var/val} ∈ θ then return UNIFY(val , x , θ)
else if {x/val} ∈ θ then return UNIFY(var , val , θ)
else if OCCUR-CHECK?(var , x ) then return failure
else return add {var /x} to θ
Figure 9.1 The unification algorithm. The algorithm works by comparing the structures of the in-
puts, element by element. Thesubstitution θ that is the argument to UNIFY is built up along the way and
is used to make sure that later comparisons are consistent with bindings that were established earlier. In
a compound expression such as F (A,B), the OP field picks out the function symbol F and the ARGS
field picks out the argument list (A,B).
23
Suposições	
  representacionais	
  do	
  Datalog	
  
¨  O	
  conhecimento	
  de	
  um	
  agente	
  pode	
  ser	
  descrito	
  de	
  forma	
  
úAl	
  em	
  termos	
  de	
  indivíduos	
  e	
  as	
  relações	
  entre	
  os	
  
indivíduos.	
  
¨  A	
  base	
  de	
  conhecimento	
  de	
  um	
  agente	
  consiste	
  de	
  
declarações	
  definidas	
  e	
  posiAvas.	
  
¨  O	
  ambiente	
  é	
  estáAco.	
  
¨  Há	
  apenas	
  um	
  número	
  finito	
  de	
  indivíduos	
  de	
  interesse	
  no	
  
domínio.	
  	
  A	
  cada	
  indivíduo	
  pode	
  ser	
  dado	
  um	
  nome	
  único.	
  
¨  ⇒	
   	
  
Sintaxe	
  do	
  Datalog	
  
¨  	
  inicia	
  com	
  letra	
  maiúscula.	
  
¨  	
  inicia	
  com	
  letra	
  minúscula	
  ou	
  é	
  uma	
  sequência	
  de	
  
dígitos	
  (numeração).	
  
¨  começa	
  com	
  letra	
  minúscula.	
  
¨  	
  é	
  uma	
  variável	
  ou	
  uma	
  constante.	
  
¨  (átomo)	
  é	
  da	
  forma	
  p	
  ou	
  p(t1,	
  …,tn),	
  onde	
  p	
  
é	
  um	
  símbolo	
  de	
  predicado	
  e	
  ti	
  são	
  termos.	
  
Sintaxe	
  do	
  Datalog(cont)	
  
¨  é	
  um	
  símbolo	
  atômico	
  (um	
  fato)	
  ou	
  
termo	
  na	
  	
  forma:	
  
	
  na	
  qual	
  a	
  e	
  bi	
  são	
  símbolos	
  atômicos.	
  
	
  
¨  	
  (query)	
  é	
  da	
  forma	
  ?	
  b1 ∧ ... ∧ bm.	
  
¨  é	
  um	
  conjunto	
  de	
  cláusulas	
  de	
  
definidas.	
  
Syntax of Datalog (cont)
definite clause is either an atomic symbol (a fact) or of the
form:
a|{z} � b1 ⇥ · · · ⇥ bm| {z }
head body
where a and bi are atomic symbols.
query is of the form ?b1 ⇥ · · · ⇥ bm.
knowledge base is a set of definite clauses.
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.1, Page 6
Exemplo	
  base	
  de	
  conhecimento	
  Example Knowledge Base
in(kim,R)�
teaches(kim, cs322) ⇥
in(cs322,R).
grandfather(william,X )�
father(william,Y ) ⇥
parent(Y ,X ).
slithy(toves)�
mimsy ⇥ borogroves ⇥
outgrabe(mome,Raths).
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.1, Page 7
SemânAca:	
  Ideia	
  Geral	
  
¨  Uma	
   	
  especifica	
  o	
  significado	
  das	
  sentenças	
  na	
  
língua.	
  
¨  Uma	
   	
  especifica:	
  
¤  quais	
  objetos	
  (indivíduos)	
  estão	
  no	
  mundo.	
  
¤  a	
  correspondência	
  entre	
  símbolos	
  no	
  computador	
  e	
  objetos	
  e	
  relações	
  
no	
  mundo.	
  
n  constantes	
  denotam	
  indivíduos	
  
n  símbolos	
  predicados	
  denotam	
  relações	
  
SemânAca	
  formal	
  
¨  Uma	
   	
  é	
  uma	
  tripla	
  I	
  =	
  <D,φ,π>,	
  onde:	
  
¤  D,	
  o	
   	
  é	
  um	
  conjunto	
  não	
  vazio.	
  	
  Elementos	
  de	
  d	
  são	
  
.	
  
¤  φ	
  é	
  um	
  mapeamento	
  que	
  atribui	
  a	
  cada	
  constante	
  um	
  elemento	
  de	
  D.	
  	
  
A	
  constante	
  c	
  denota	
  o	
  individuo	
  φ(c).	
  
¤  π	
  é	
  um	
  mapeamento	
  que	
  atribui	
  a	
  cada	
  símbolo	
  de	
  predicado	
  n-­‐ário	
  
uma	
  relação:	
  uma	
  função	
  de	
  Dn	
  em	
  {TRUE,	
  FALSE}.	
  
Exemplo	
  de	
  interpretação	
  Example Interpretation
Constants: phone, pencil , telephone.
Predicate Symbol: noisy (unary), left of (binary).
D = {",%,.}.
⇥(phone) =%, ⇥(pencil) =., ⇥(telephone) =%.
�(noisy): �"⇥ FALSE �%⇥ TRUE �.⇥ FALSE
�(left of ):
�","⇥ FALSE �",%⇥ TRUE �",.⇥ TRUE
�%,"⇥ FALSE �%,%⇥ FALSE �%,.⇥ TRUE
�.,"⇥ FALSE �.,%⇥ FALSE �.,.⇥ FALSE
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.2, Page 3
Pontos	
  importantes	
  a	
  serem	
  observados	
  
¨  O	
  domínio	
  D	
  pode	
  conter	
  objetos	
  reais.	
  	
  (e.g.,	
  uma	
  pessoa,	
  
uma	
  sala,	
  um	
  curso).	
  	
  D	
  não	
  necessariamente	
  pode	
  ser	
  
armazenado	
  em	
  um	
  computador.	
  
¨  π(p)	
  especifica	
  se	
  a	
  relação	
  denotada	
  pelo	
  símbolo	
  de	
  
predicado	
  n-­‐ário	
  p	
  é	
  verdadeira	
  ou	
  falsa	
  para	
  cada	
  n-­‐tupla	
  de	
  
indivíduos.	
  
¨  Se	
  o	
  símbolo	
  predicado	
  p	
  não	
  tem	
  argumentos,	
  então	
  π(p)	
  é	
  
TRUE	
  ou	
  FALSE.	
  
Verdade	
  em	
  uma	
  interpretação	
  
¨  Uma	
  constante	
  c	
   o	
  indivíduo	
  φ(c).	
  
¨  O	
  átomo	
  fundamental	
  (livre	
  de	
  variável)	
  p(t1,	
  …,tn)	
  é:	
  
¤  se	
  π(p)(	
  φ(t1),	
  …,φ(tn)	
  )	
  =	
  TRUE	
  na	
  
interpretação	
  I	
  e	
  
¤  	
  caso	
  contrário.	
  
¨  A	
  cláusula	
  fundamental	
  h	
  ←	
  b1	
  ∧	
  …	
  ∧	
  bm	
  é	
  
se	
  h	
  é	
  falso	
  em	
  I	
  e	
  cada	
  bi	
  é	
  verdadeiro	
  em	
  I	
  e	
  
é	
   caso	
  contrário.	
  
Exemplo	
  de	
  verdades	
  
¨  Na	
  interpretação	
  dada	
  antes:	
  
Example Truths
In the interpretation given before:
noisy(phone) true
noisy(telephone) true
noisy(pencil) false
left of (phone, pencil) true
left of (phone, telephone) false
noisy(pencil)� left of (phone, telephone) true
noisy(pencil)� left of (phone, pencil) false
noisy(phone)� noisy(telephone) ⇥ noisy(pencil) true
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.2, Page 6
Modelos	
  e	
  consequências	
  lógicas	
  
¨  Uma	
  base	
  de	
  conhecimento,	
  BC,	
  é	
  verdade	
  na	
  interpretação	
  I	
  
se	
  e	
  somente	
  se	
  cada	
  cláusula	
  em	
  BC	
  é	
  verdade	
  em	
  I.	
  
¨  Um	
   	
  de	
  um	
  conjunto	
  de	
  cláusulas	
  é	
  uma	
  
interpretação	
  em	
  que	
  todas	
  as	
  cláusulas	
  são	
  verdadeiras.	
  
¨  Se	
  BC	
  é	
  um	
  conjunto	
  de	
  cláusulas	
  e	
  g	
  é	
  um	
  conjunto	
  de	
  
átomos,	
  g	
  é	
  uma	
   de	
  BC,	
  escrito	
   ,	
  
se	
  g	
  é	
  verdade	
  em	
  todos	
  os	
  modelos	
  de	
  BC.	
  
¨  Ou	
  seja,	
  BC	
  |=	
  g	
  se	
  não	
  há	
  nenhuma	
  interpretação	
  onde	
  BC	
  é	
  
verdadeira	
  e	
  g	
  é	
  falsa.	
  
Visão	
  do	
  usuário	
  da	
  semânAca	
  
1.  Escolha	
  um	
  domínio	
  de	
  tarefa:	
   .	
  
2.  Associe	
  constantes	
  com	
  os	
  indivíduos	
  que	
  você	
  deseja	
  
nomear.	
  
3.  Para	
  cada	
  relação	
  que	
  você	
  pretende	
  representar,	
  associe	
  
um	
  símbolo	
  predicado	
  na	
  linguagem.	
  
4.  Forneça	
  ao	
  sistema	
  cláusulas	
  que	
  são	
  verdadeiras	
  na	
  
interpretação	
  pretendida:	
   .	
  
5.  Faça	
  perguntas	
  sobre	
  a	
  interpretação	
  pretendida.	
  
6.  Se	
  KB	
  |=	
  g,	
  então	
  g	
  deve	
  ser	
  verdade	
  na	
  interpretação	
  
pretendida.	
  
Visão	
  do	
  computador	
  da	
  semânAca	
  
¨  O	
  computador	
  não	
  tem	
  acesso	
  a	
  interpretação	
  pretendida.	
  
¨  Tudo	
  o	
  que	
  ele	
  sabe	
  é	
  a	
  base	
  de	
  conhecimento.	
  
¨  O	
  computador	
  pode	
  determinar	
  se	
  uma	
  fórmula	
  é	
  uma	
  
consequência	
  lógica	
  da	
  BC.	
  
¨  Se	
  BC	
  |=	
  g	
  então	
  g	
  deve	
  serverdade	
  na	
  interpretação	
  
pretendida.	
  
¨  Se	
  BC	
  |≠	
  g,	
  então	
  há	
  um	
  modelo	
  de	
  BC	
  em	
  que	
  g	
  é	
  falsa.	
  Esta	
  
poderia	
  ser	
  a	
  interpretação	
  pretendida.	
  
O	
  papel	
  da	
  semânAca	
  em	
  um	
  SRR	
  Role of Semantics in an RRS
����������
��������
�������������
����������������
���������
�����	��k�
������������
�	��˜
���������
��
���
����
����
���
�������
�������
������������
���������
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.2, Page 10
Variáveis	
  
¨  Variáveis	
  são	
   no	
  escopo	
  de	
  
uma	
  cláusula.	
  
¨  Uma	
   é	
  uma	
  função	
  de	
  variáveis	
  para	
  o	
  
domínio.	
  
¨  Dada	
  uma	
  interpretação	
  e	
  uma	
  atribuição	
  de	
  variável,	
  
	
  cada	
  termo	
  denota	
  um	
  indivíduo	
  e	
  
	
  cada	
  cláusula	
  é	
  TRUE	
  ou	
  FALSE.	
  
¨  Uma	
  cláusula	
  contendo	
  variáveis	
  é	
  verdadeira	
  em	
  uma	
  
interpretação,	
  se	
  é	
  verdade	
   as	
  atribuições	
  de	
  
variáveis.	
  
Consultas	
  (queries)	
  e	
  respostas	
  
¨  Uma	
   	
  é	
  uma	
  forma	
  de	
  perguntar	
  se	
  um	
  corpo	
  é	
  uma	
  
consequência	
  lógica	
  da	
  base	
  de	
  conhecimento:	
  
	
   	
  ?b1 ∧ … ∧ bm. 
¨  Uma	
   	
  ou	
  é	
  
¤  uma	
  instância	
  da	
  consulta	
  que	
  é	
  uma	
  consequência	
  lógica	
  da	
  base	
  de	
  
conhecimento	
  KB,	
  ou	
  
¤  	
   se	
  nenhuma	
  instância	
  é	
  uma	
  consequência	
  lógica	
  do	
  KB.	
  
Exemplos	
  de	
  consultas	
  
Example Queries
KB =
8<: in(kim, r123).part of (r123, cs building).
in(X ,Y )� part of (Z ,Y ) ⇥ in(X ,Z ).
Query Answer
?part of (r123,B).
part of (r123, cs building)
?part of (r023, cs building). no
?in(kim, r023). no
?in(kim,B). in(kim, r123)
in(kim, cs building)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 3
Exemplos	
  de	
  consultas	
  
Example Queries
KB =
8<: in(kim, r123).part of (r123, cs building).
in(X ,Y )� part of (Z ,Y ) ⇥ in(X ,Z ).
Query Answer
?part of (r123,B). part of (r123, cs building)
?part of (r023, cs building).
no
?in(kim, r023). no
?in(kim,B). in(kim, r123)
in(kim, cs building)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 4
Exemplos	
  de	
  consultas	
  
Example Queries
KB =
8<: in(kim, r123).part of (r123, cs building).
in(X ,Y )� part of (Z ,Y ) ⇥ in(X ,Z ).
Query Answer
?part of (r123,B). part of (r123, cs building)
?part of (r023, cs building). no
?in(kim, r023).
no
?in(kim,B). in(kim, r123)
in(kim, cs building)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 5
Exemplos	
  de	
  consultas	
  
Example Queries
KB =
8<: in(kim, r123).part of (r123, cs building).
in(X ,Y )� part of (Z ,Y ) ⇥ in(X ,Z ).
Query Answer
?part of (r123,B). part of (r123, cs building)
?part of (r023, cs building). no
?in(kim, r023). no
?in(kim,B).
in(kim, r123)
in(kim, cs building)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 6
Exemplos	
  de	
  consultas	
  
Example Queries
KB =
8<: in(kim, r123).part of (r123, cs building).
in(X ,Y )� part of (Z ,Y ) ⇥ in(X ,Z ).
Query Answer
?part of (r123,B). part of (r123, cs building)
?part of (r023, cs building). no
?in(kim, r023). no
?in(kim,B). in(kim, r123)
in(kim, cs building)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 7
Consequência	
  lógica	
  
¨  Um	
  átomo	
  g	
  é	
  uma	
  consequência	
  lógica	
  da	
  BC	
  se	
  e	
  somente	
  
se:	
  
¤  g	
  é	
  um	
  fato	
  na	
  BC,	
  ou	
  
¤  existe	
  uma	
  regra	
  
	
   	
  g	
  ←	
  b1	
  ∧	
  …	
  ∧	
  bk	
  
	
  na	
  BC	
  que	
  cada	
  bi	
  é	
  uma	
  consequência	
  lógica	
  da	
  BC	
  
Depurando	
  falsas	
  conclusões	
  
¨  Para	
  depurar	
  uma	
  resposta	
  g	
  que	
  é	
  falsa	
  na	
  interpretação	
  
pretendida:	
  
¤  Se	
  g	
  é	
  um	
  fato	
  em	
  BC,	
  este	
  fato	
  é	
  errado.	
  
¤  Caso	
  contrário,	
  suponha	
  que	
  g	
  foi	
  provada	
  usando	
  a	
  regra:	
  
	
   	
  g	
  ←	
  b1	
  ∧	
  …	
  ∧	
  bk	
  
	
  onde	
  cada	
  bi	
  é	
  uma	
  consequência	
  lógica	
  do	
  BC.	
  
	
  Se	
  cada	
  bi	
  é	
  verdade	
  na	
  interpretação	
  pretendida,	
  esta	
  
	
  cláusula	
  é	
  falsa	
  na	
  interpretação	
  pretendida.	
  
	
  Se	
  algum	
  bi	
  é	
  falso	
  na	
  interpretação	
  pretendida,	
  depure	
  	
  bi.	
  
Cláusulas	
  definidas	
  de	
  primeira	
  ordem	
  
¨  Nem	
  toda	
  BC	
  pode	
  ser	
  converAda	
  em	
  um	
  conjunto	
  de	
  
cláusulas	
  definidas,	
  mas	
  é	
  possível	
  converter	
  muitas	
  delas.	
  
¤  O	
  custo	
  da	
  conversão	
  é	
  compensado	
  pela	
  eficiência	
  do	
  algoritmo	
  de	
  
encadeamento	
  para	
  frente	
  (linear)	
  
¨  Considere	
  o	
  problema:	
  
¤  A	
  lei	
  diz	
  que	
  é	
  crime	
  um	
  americano	
  vender	
  armas	
  para	
  nações	
  hosAs.	
  
O	
  país	
  nono,	
  um	
  inimigo	
  da	
  América,	
  tem	
  alguns	
  mísseis,	
  e	
  todos	
  
foram	
  vendidos	
  pelo	
  Coronel	
  West,	
  que	
  é	
  um	
  americano.	
  
46 
Cláusulas	
  definidas	
  de	
  primeira	
  ordem	
  
¨  …	
  é	
  crime	
  para	
  um	
  americano	
  vender	
  armas	
  para	
  nações	
  hosAs:	
  
¨  (1) americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ hostil(Z) => criminoso(X) 
¨  nono…	
  tem	
  alguns	
  mísseis:	
  	
  
¨  ∃x proprietário(nono, x) ٨۸ míssil(x) 
¨  (2) proprietário(nono, M1) ٨۸ míssil(M1) 
¨  …	
  todos	
  estes	
  mísseis	
  foram	
  vendidos	
  para	
  ele	
  pelo	
  Coronel	
  West:	
  
¨  (3) míssil(X) ٨۸ proprietário(nono,X) => vende(west,X,nono) 
47 
Cláusulas	
  definidas	
  de	
  primeira	
  ordem	
  
¨  Mísseis	
  são	
  armas:	
  
¨  (4) míssil(X) => arma(X)‏ 
¨  Um	
  inimigo	
  da	
  América	
  é	
  considerado	
  hosAl:	
  
¨  (5) inimigo(X,américa) => hostil(X)‏ 
¨  West,	
  que	
  é	
  americano…	
  
¨  (6) americano(west)‏ 
¨  O	
  país	
  	
  Nono,	
  é	
  um	
  inimigo	
  da	
  América	
  
¨  (7) inimigo(nono,américa)‏ 
48 
Ambiente	
  elétrico	
  
Electrical Environment
�����
�����
�
������
������
���
��
�����
������
�����������
���
�����
�������
���
��
��
�� ��
��
��
��
��
��
��
��
��
���
�	
��
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 10
AxiomaAzando	
  o	
  ambiente	
  elétrico	
  Axiomatizing the Electrical Environment
% light(L) is true if L is a light
light(l1). light(l2).
% down(S) is true if switch S is down
down(s1). up(s2). up(s3).
% ok(D) is true if D is not broken
ok(l1). ok(l2). ok(cb1). ok(cb2).
?light(l1). =�
yes
?light(l6). =� no
?up(X ). =� up(s2), up(s3)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 11
AxiomaAzando	
  o	
  ambiente	
  elétrico	
  Axiomatizing the Electrical Environment
% light(L) is true if L is a light
light(l1). light(l2).
% down(S) is true if switch S is down
down(s1). up(s2). up(s3).
% ok(D) is true if D is not broken
ok(l1). ok(l2). ok(cb1). ok(cb2).
?light(l1). =� yes
?light(l6). =�
no
?up(X ). =�up(s2), up(s3)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 12
AxiomaAzando	
  o	
  ambiente	
  elétrico	
  Axiomatizing the Electrical Environment
% light(L) is true if L is a light
light(l1). light(l2).
% down(S) is true if switch S is down
down(s1). up(s2). up(s3).
% ok(D) is true if D is not broken
ok(l1). ok(l2). ok(cb1). ok(cb2).
?light(l1). =� yes
?light(l6). =� no
?up(X ). =�
up(s2), up(s3)
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 13
Exemplo:	
  o	
  ambiente	
  elétrico	
  
connected to(X ,Y ) is true if component X is connected to Y
connected to(w0,w1)� up(s2).
connected to(w0,w2)� down(s2).
connected to(w1,w3)� up(s1).
connected to(w2,w3)� down(s1).
connected to(w4,w3)� up(s3).
connected to(p1,w3).
?connected to(w0,W ). =⇥
W = w1
?connected to(w1,W ). =⇥ no
?connected to(Y ,w3). =⇥ Y = w2, Y = w4, Y = p1
?connected to(X ,W ). =⇥ X = w0,W = w1, . . .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 15
Exemplo:	
  o	
  ambiente	
  elétrico	
  
connected to(X ,Y ) is true if component X is connected to Y
connected to(w0,w1)� up(s2).
connected to(w0,w2)� down(s2).
connected to(w1,w3)� up(s1).
connected to(w2,w3)� down(s1).
connected to(w4,w3)� up(s3).
connected to(p1,w3).
?connected to(w0,W ). =⇥ W = w1
?connected to(w1,W ). =⇥
no
?connected to(Y ,w3). =⇥ Y = w2, Y = w4, Y = p1
?connected to(X ,W ). =⇥ X = w0,W = w1, . . .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 16
Exemplo:	
  o	
  ambiente	
  elétrico	
  
connected to(X ,Y ) is true if component X is connected to Y
connected to(w0,w1)� up(s2).
connected to(w0,w2)� down(s2).
connected to(w1,w3)� up(s1).
connected to(w2,w3)� down(s1).
connected to(w4,w3)� up(s3).
connected to(p1,w3).
?connected to(w0,W ). =⇥ W = w1
?connected to(w1,W ). =⇥ no
?connected to(Y ,w3). =⇥
Y = w2, Y = w4, Y = p1
?connected to(X ,W ). =⇥ X = w0,W = w1, . . .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 17
Exemplo:	
  o	
  ambiente	
  elétrico	
  
connected to(X ,Y ) is true if component X is connected to Y
connected to(w0,w1)� up(s2).
connected to(w0,w2)� down(s2).
connected to(w1,w3)� up(s1).
connected to(w2,w3)� down(s1).
connected to(w4,w3)� up(s3).
connected to(p1,w3).
?connected to(w0,W ). =⇥ W = w1
?connected to(w1,W ). =⇥ no
?connected to(Y ,w3). =⇥ Y = w2, Y = w4, Y = p1
?connected to(X ,W ). =⇥
X = w0,W = w1, . . .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 18
Exemplo:	
  o	
  ambiente	
  elétrico	
  
connected to(X ,Y ) is true if component X is connected to Y
connected to(w0,w1)� up(s2).
connected to(w0,w2)� down(s2).
connected to(w1,w3)� up(s1).
connected to(w2,w3)� down(s1).
connected to(w4,w3)� up(s3).
connected to(p1,w3).
?connected to(w0,W ). =⇥ W = w1
?connected to(w1,W ). =⇥ no
?connected to(Y ,w3). =⇥ Y = w2, Y = w4, Y = p1
?connected to(X ,W ). =⇥ X = w0,W = w1, . . .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.3, Page 19
Exemplo:	
  o	
  ambiente	
  elétrico	
  
% lit(L) is true if the light L is lit 
 
 lit(L) ← light(L) ∧ ok(L) ∧ live(L). 
 
% live(C) is true if there is power coming into C 
 
 live(Y) ← 
 connected to(Y,Z) ∧ 
 live(Z). 
 live(outside). 
¨  Esta	
  é	
  uma	
   de	
  live.	
  
Provas	
  
¨  Uma	
   	
  é	
  uma	
  demonstração	
  mecanicamente	
  derivável	
  de	
  que	
  
uma	
  fórmula	
  decorre	
  logicamente	
  de	
  uma	
  base	
  de	
  conhecimento.	
  
¨  Tendo	
  em	
  conta	
  um	
  procedimento	
  prova,	
   significa	
  g	
  pode	
  ser	
  
deduzido	
  da	
  base	
  de	
  conhecimento	
  BC.	
  
¨  Lembre-­‐se	
  de	
   g	
  significa	
  g	
  é	
  verdade	
  em	
  todos	
  os	
  modelos	
  de	
  
BC.	
  
¨  Um	
  procedimento	
  de	
  prova	
  é	
   se	
  KB	
  ⊢	
  g	
  implica	
  KB	
  |=	
  g.	
  	
  
¨  Um	
  procedimento	
  de	
  prova	
  é	
   	
  se	
  KB	
  |=	
  g	
  implica	
  KB	
  ⊢	
  g.	
  
BC	
  exemplo	
  
¨  (1) americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ hostil(Z) => criminoso(X) 
¨  (2) proprietário(nono,M1) ٨۸ míssil(M1) 
¨  (3) míssil(X) ٨۸ proprietário(nono,X) => vende(west,X,nono) 
¨  (4) míssil(X) => arma(X)‏ 
¨  (5) inimigo(X,américa) => hostil(X)‏ 
¨  (6) americano(west)‏ 
¨  (7) inimigo(nono,américa)‏ 
60 
Exemplo:Encadeamento	
  para	
  frente	
  
(BoCom-­‐up)	
  
¨  Vamos	
  provar	
  que	
  West	
  é	
  criminoso	
  =	
  criminoso(west).	
  
¨  Inicialmente	
  temos	
  os	
  fatos	
  derivados	
  de	
  (2),	
  (6)	
  e	
  (7):	
  
¤  {proprietário(nono,m1), míssil(m1), americano(west)‏, inimigo(nono, 
américa)}	
  
¨  De	
  (2)	
  proprietário(nono, m1) ٨۸ míssil(m1)‏ e	
  de	
  (3)	
  míssil(X) ٨۸ 
proprietário(nono,X) => vende(west,X,nono) 
¤  Com	
  {X/m1},	
  adicionamos	
  (8)	
  vende(west,m1,nono).	
  
¤  {proprietário(nono,m1), míssil(m1), americano(west)‏, inimigo(nono, 
américa), vende(west m1,nono)}	
  
¨  De	
  (2)	
  proprietário(nono,m1) ٨۸ míssil(m1)‏ e	
  de	
  (4)	
  míssil(X) => arma(X) 
¤  Com {X/m1}, adicionamos (9) arma(m1).	
  
¤  {proprietário(nono,m1), míssil(m1), americano(west)‏, inimigo(nono, 
américa), vende(west,m1,nono), arma(m1)}	
  
61 
Exemplo:Encadeamento	
  para	
  frente	
  
(BoCom-­‐up)	
  
¨  De	
  (5)	
  inimigo(X,américa) => hostil(X) e	
  de	
  (7)	
  inimigo(nono, américa)‏ 
¤  Com {X/nono}, adicionamos (10) hostil(nono).	
  
¤  {proprietário(nono,m1), míssil(m1), americano(west)‏, inimigo(nono, 
américa), vende(west,m1,nono), arma(m1), hostil(nono)}	
  
¨  De	
  (1)	
  americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ hostil(Z) => criminoso(X) e	
  
de	
  (6)	
  americano(west),	
  (9)	
  arma(m1),	
  (8)	
  vende(west,m1,nono) e	
  (10)	
  
hostil(nono)‏ 
¤  Com	
  {X/west,	
  Y/m1,	
  Z/nono},	
  adicionamos	
  criminoso(west).	
  
¤  {proprietário(nono,m1), míssil(m1), americano(west)‏, inimigo(nono, 
américa), vende(west,m1,nono), arma(M1), hostil(nono), criminoso(west)}	
  
n  criminoso(west) não	
  é	
  premissa	
  de	
  nenhuma	
  cláusula	
  então	
  este	
  é	
  o	
  conjunto	
  
Ponto	
  Fixo	
  da	
  BC.	
  	
  
62 
Árvore	
  de	
  derivação	
  (boCom-­‐up)	
  
Hostile(Nono)
Enemy(Nono,America)Owns(Nono,M1)Missile(M1)
Criminal(West)
Missile(y)
Weapon(y) Sells(West,M1,z)American(West)
{y/M1} { }{ }{ }
 {z/Nono}{ }
AlgorAmo	
  de	
  encadeamento	
  p/	
  frente	
  
24 Chapter 9. Inference in First-Order Logic
function FOL-FC-ASK(KB ,α) returns a substitution or false
inputs: KB , the knowledge base, a set of first-order definite clauses
α, the query, an atomic sentence
local variables: new , the new sentences inferred on each iteration
repeat until new is empty
new← { }
for each rule in KB do
(p1 ∧ . . . ∧ pn ⇒ q)← STANDARDIZE-VARIABLES(rule)
for each θ such that SUBST(θ,p1 ∧ . . . ∧ pn) = SUBST(θ,p′1 ∧ . . . ∧ p′n)
for some p′1, . . . , p′n in KB
q ′← SUBST(θ, q)
if q ′ does not unify with some sentence already in KB or new then
add q ′ to new
φ←UNIFY(q ′,α)
if φ is not fail then return φ
add new to KB
return false
Figure 9.3 A conceptually straightforward, but very inefficient, forward-chaining algorithm. On
each iteration, it adds to KB all the atomic sentences that can be inferred in one step from the impli-
cation sentences and the atomic sentences already in KB . The function STANDARDIZE-VARIABLES
replaces all variables in its arguments with new ones that have not been used before.function FOL-BC-ASK(KB , query ) returns a generator of substitutions
return FOL-BC-OR(KB , query ,{ })
generator FOL-BC-OR(KB , goal , θ) yields a substitution
for each rule (lhs ⇒ rhs) in FETCH-RULES-FOR-GOAL(KB , goal ) do
(lhs , rhs)← STANDARDIZE-VARIABLES((lhs , rhs))
for each θ′ in FOL-BC-AND(KB , lhs , UNIFY(rhs , goal , θ)) do
yield θ′
generator FOL-BC-AND(KB , goals , θ) yields a substitution
if θ = failure then return
else if LENGTH(goals) = 0 then yield θ
else do
first ,rest← FIRST(goals), REST(goals)
for each θ′ in FOL-BC-OR(KB , SUBST(θ, first ), θ) do
for each θ′′ in FOL-BC-AND(KB , rest , θ′) do
yield θ′′
Figure 9.6 A simple backward-chaining algorithm for first-order knowledge bases.
Exemplo	
  
Example
live(Y )� connected to(Y ,Z ) ⇥ live(Z ). live(outside).
connected to(w6,w5). connected to(w5, outside).
C = {live(outside),
connected to(w6,w5),
connected to(w5, outside),
live(w5),
live(w6)}
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.4, Page 7
Exemplo	
  
Example
live(Y )� connected to(Y ,Z ) ⇥ live(Z ). live(outside).
connected to(w6,w5). connected to(w5, outside).
C = {live(outside),
connected to(w6,w5),
connected to(w5, outside),
live(w5),
live(w6)}
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.4, Page 8
Consistência	
  do	
  procedimento	
  de	
  prova	
  
BoCom-­‐up	
  
¨  Suponha	
  que	
  existe	
  um	
  g	
  tal	
  que	
  KB	
  ⊢	
  g	
  e	
  KB	
  |≠	
  g.	
  
¨  Logo,	
  deve	
  haver	
  um	
  primeiro	
  átomo	
  adicionado	
  a	
  C	
  que	
  tem	
  uma	
  
instância	
  que	
  não	
  é	
  verdade	
  em	
  todos	
  os	
  modelos	
  de	
  BC.	
  	
  Chame-­‐o	
  de	
  h.	
  
Suponha	
  que	
  h	
  não	
  é	
  verdadeiro	
  no	
  modelo	
  I	
  do	
  BC.	
  
¨  Deve	
  haver	
  uma	
  cláusula	
  em	
  BC	
  da	
  forma	
  
 h’ ← b1 ∧ ... ∧ bm 
¨  onde	
  h	
  =	
  h’θ.	
  	
  Cada	
  bi	
  é	
  verdade	
  em	
  I.	
  	
  h	
  é	
  falso	
  em	
  I.	
  	
  Assim,	
  esta	
  cláusula	
  
é	
  falsa	
  em	
  I.	
  	
  Portanto	
  I	
  não	
  é	
  um	
  modelo	
  de	
  BC.	
  
¨  Contradição.	
  
Ponto	
  fixo	
  
¨  O	
  C	
  gerado	
  pelo	
  algoritmo	
  BoCom-­‐up	
  é	
  chamado	
  de	
   .	
  
¨  C	
  pode	
  ser	
  infinito;	
  exigimos	
  que	
  a	
  seleção	
  seja	
  justa.	
  
¨  :	
  o	
  domínio	
  é	
  o	
  conjunto	
  de	
  constantes.	
  
Inventamos	
  uma	
  se	
  a	
  BC	
  ou	
  a	
  consulta	
  não	
  conAver	
  uma.	
  Cada	
  constante	
  
denota	
  a	
  si	
  mesma.	
  
¨  Deixe	
  I	
  ser	
  a	
  interpretação	
  de	
  Herbrand	
  em	
  que	
  cada	
  instância	
  fundamental	
  
de	
  cada	
  elemento	
  do	
  ponto	
  fixo	
  é	
  TRUE	
  e	
  cada	
  outro	
  átomo	
  é	
  FALSE.	
  
¨  I	
  é	
  um	
  modelo	
  de	
  BC.	
  
¨  	
  Prova:	
  suponha	
  que	
  h	
  ←	
  b1	
  ∧	
  ...	
  ∧	
  bm	
  na	
  BC	
  é	
  falso	
  em	
  I.	
  	
  Então,	
  h	
  é	
  falso	
  e	
  
	
  cada	
  bi	
  é	
  verdadeiro	
  em	
  I.	
  	
  Assim,	
  h	
  pode	
  ser	
  adicionado	
  a	
  C.	
  Contadiz	
  o	
  fato	
  
	
  de	
  C	
  ser	
  o	
  ponto	
  de	
  fixo.	
  
¨  I	
  é	
  chamado	
  de	
  um	
   .	
  
Completude	
  
¨  Suponha	
  que	
  BC	
  |=	
  g.	
  	
  Em	
  seguida,	
  g	
  é	
  verdade	
  em	
  todos	
  os	
  
modelos	
  de	
  BC.	
  
¨  Assim,	
  g	
  é	
  verdade	
  no	
  modelo	
  mínimo.	
  
¨  Assim,	
  g	
  é	
  o	
  ponto	
  de	
  fixo.	
  
¨  Assim,	
  g	
  é	
  gerado	
  pelo	
  algoritmo	
  BoCom-­‐up.	
  
Eficiência	
  do	
  encadeamento	
  p/	
  frente	
  
¨  É	
   .	
  
¤  Toda	
  inferência	
  é	
  uma	
  aplicação	
  de	
  Modus	
  Ponens	
  Generalizado.	
  
¨  É	
   	
  para	
  BCs	
  de	
  cláusulas	
  definidas.	
  
¤  Para	
  BCs	
  que	
  são	
  Datalog,	
  é	
  completo	
  –	
  a	
  prova	
  da	
  consequência	
  
lógica	
  é	
  decidível.	
  
¤  Para	
  BCs	
  que	
  contém	
  símbolos	
  de	
  funções,	
  a	
  prova	
  da	
  consequência	
  
lógica	
  é	
  semidecidível.	
  
70 
Encadeamento	
  p/	
  frente	
  eficiente	
  
¨  Pontos	
  que	
  podem	
  ser	
  melhorados:	
  
¤  O	
  laço	
  interno	
  do	
  algoritmo	
  ASK-­‐LPO-­‐EF	
  envolve	
  a	
  localização	
  de	
  todos	
  
os	
  unificadores	
  tais	
  que	
  a	
  premissa	
  de	
  uma	
  regra	
  se	
  unifica	
  com	
  um	
  
conjunto	
  adequado	
  de	
  fatos	
  na	
  BC.	
  
¤  ASK-­‐LPO-­‐EF	
  verifica	
  exausAvamente	
  cada	
  regra	
  em	
  toda	
  iteração	
  para	
  
ver	
  se	
  suas	
  premissas	
  são	
  saAsfeitas,	
  ainda	
  que	
  muito	
  poucas	
  adições	
  
tenham	
  sido	
  feitas	
  à	
  BC.	
  
¤  ASK-­‐LPO-­‐EF	
  poderia	
  gerar	
  muitos	
  fatos	
  irrelevantes	
  para	
  o	
  objeAvo.	
  
71 
Comparação	
  entre	
  regras	
  e	
  fatos	
  
conhecidos	
  
¨  Supõe	
  a	
  sentença:	
  
¤  míssil(X) ٨۸ proprietário(nono,X) ٨۸ vende(west,X,nono)‏ 
¨  Precisamos	
  encontrar	
  todos	
  os	
  fatos	
  que	
  se	
  unificam	
  com	
  míssil(X),	
  para	
  
encontrar	
  todo	
  objeto	
  que	
  é	
  um	
  míssil.	
  	
  
¤  Em	
  uma	
  BC	
  indexada	
  de	
  forma	
  adequada	
  isso	
  pode	
  ser	
  feito	
  em	
  tempo	
  
constante.	
  
¨  Depois,	
  temos	
  que	
  verificar	
  se	
  esses	
  mísseis	
  pertencem	
  à	
  nono.	
  	
  
¤  Mas	
  se	
  houver	
  muitos	
  mísseis	
  e	
  poucos	
  deles	
  forem	
  de	
  nono,	
  será	
  melhor	
  
encontrar	
  quais	
  objetos	
  pertencem	
  à	
  nono,	
  e	
  depois	
  verificar	
  se	
  eles	
  são	
  
mísseis.	
  
–	
  é	
  NP-­‐di‰cil,	
  mas	
  existem	
  boas	
  
heurísAcas	
  (variável	
  mais	
  restrita).	
  
¤  Correspondência	
  de	
  padrões	
  e	
  PSRs.	
  
72 
Encadeamento	
  p/	
  frente	
  incremental	
  
¨  Não	
  precisamos	
  verificar	
  exausAvamente	
  cada	
  regra	
  em	
  toda	
  iteração	
  do	
  
algoritmo.	
  
¨  Qualquer	
  inferência	
  que	
  não	
  exigisse	
  um	
  fato	
  novo	
  na	
  iteração	
  t	
  –	
  1	
  já	
  foi	
  
deduzido	
  até	
  essa	
  iteração.	
  
¨  Assim,	
  na	
  iteração	
  t	
  verificamos	
  apenas	
  as	
  regras	
  que	
  possuem	
  em	
  sua	
  
premissa	
  um	
  elemento	
  pi	
  que	
  se	
  unifica	
  com	
  um	
  fato	
  p'i	
  recém-­‐deduzido	
  
na	
  iteração	
  t	
  –	
  1.	
  
¨  Esse	
  algoritmo	
  gera	
  exatamente	
  os	
  mesmos	
  fatos	
  de	
  	
  ASK-­‐LPO-­‐EF	
  mais	
  é	
  
muito	
  mais	
  eficiente.	
  
¨  Muitos	
  sistemas	
  reais	
  operam	
  em	
  um	
  modo	
  de	
  “atualização”	
  em	
  que	
  
ocorre	
  o	
  EF	
  em	
  resposta	
  a	
  cada	
  fato	
  novo	
  que	
  seja	
  informado	
  (com	
  TELL)	
  
ao	
  sistema.	
  
73 
Encadeamento	
  p/	
  frente	
  incremental	
  
¨  Muito	
  trabalho	
  redundante	
  é	
  feito	
  na	
  construção	
  repeAda	
  de	
  
correspondências	
  parciais	
  que	
  tem	
  algumas	
  premissas	
  não	
  saAsfeitas.	
  
¨  Exemplo:	
  Na	
  primeira	
  iteração	
  de	
  ASK-­‐LPO-­‐EF	
  uma	
  correspondência	
  parcial	
  
é	
  construída	
  entre:	
  
¤  A	
  regra	
  americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ hostil(Z) => criminoso(X)‏ 
e	
  o	
  fatoamericano(west),	
  sem	
  sucesso.	
  
¤  Mas	
  esta	
  correspondência	
  parcial	
  é	
  abandonada	
  e	
  reconstruída	
  na	
  segunda	
  
iteração,	
  quando	
  ela	
  tem	
  sucesso.	
  
¨  É	
  melhor	
  reter	
  as	
  correspondências	
  parciais	
  e	
  completá-­‐las	
  gradualmente	
  à	
  
medida	
  que	
  chegam	
  novos	
  fatos.	
  
¤  O	
   faz	
  um	
  pré-­‐processamento	
  das	
  regras	
  da	
  BC	
  e	
  funciona	
  como	
  
um	
  fluxo	
  de	
  dados	
  no	
  momento	
  da	
  avaliação.	
  
74 
Fatos	
  irrelevantes	
  
¨  O	
  EF	
  faz	
  todas	
  as	
  inferência	
  permissíveis	
  a	
  parAr	
  dos	
  fatos,	
  mesmo	
  que	
  
elas	
  sejam	
  irrelevantes	
  par	
  o	
  objeAvo.	
  
¨  Uma	
  solução	
  seria	
  fazer	
  ET.	
  
¨  Uma	
  outra	
  solução	
  é	
  restringir	
  o	
  EF	
  para	
  que	
  ele	
  trabalhe	
  somente	
  com	
  as	
  
regras	
  que	
  são	
  relevantes	
  para	
  o	
  objeAvo.	
  
¤  :	
  reescrever	
  o	
  conjunto	
  de	
  regras,	
  uAlizando	
  informações	
  do	
  objeAvo,	
  de	
  
modo	
  que	
  apenas	
  informações	
  de	
  variáveis	
  relevantes	
  sejam	
  consideradas	
  
durante	
  o	
  EF.	
  
n  Essas	
  regras	
  são	
  denominadas	
  de	
   .	
  
¤  A	
  ideia	
  é	
  fazer	
  um	
  encadeamento	
  p/	
  trás	
  “genérico”	
  a	
  fim	
  de	
  determinar	
  quais	
  
vinculações	
  de	
  variáveis	
  precisam	
  ser	
  limitadas.	
  
75 
Encadeamento	
  para	
  trás	
  (Top-­‐down)	
  
¨  É	
  muito	
  semelhante	
  ao	
  encadeamento	
  para	
  trás	
  em	
  LP.	
  
¤  Começamos	
  da	
  consulta	
  para	
  os	
  fatos.	
  
¨  O	
  algoritmo	
  uAliza	
  uma	
  pilha	
  de	
  objeAvos.	
  
¨  Cada	
  cláusula	
  na	
  qual	
  a	
  cabeça	
  se	
  unifica	
  com	
  o	
  objeAvo	
  da	
  pilha,	
  gera	
  
uma	
  chamada	
  recursiva,	
  adicionando	
  o	
  seu	
  corpo	
  à	
  pilha	
  de	
  objeAvos.	
  
¨  O	
  algoritmo	
  termina	
  porque	
  fatos	
  são	
  regras	
  que	
  não	
  tem	
  corpo	
  e,	
  
portanto,	
  não	
  adicionam	
  nada	
  à	
  pilha	
  de	
  objeAvos.	
  
¨  COMPOR(θ1,	
  θ2)	
  é	
  a	
  subsAtuição	
  cujo	
  efeito	
  é	
  idênAco	
  ao	
  efeito	
  de	
  aplicar	
  
cada	
  subsAtuição	
  separadamente.	
  
76 
Procedimento	
  de	
  prova	
  Top-­‐down	
  
¨  Uma	
   é	
  da	
  forma	
  
	
  yes(t1, …, tk) ← a1 ∧ a2 ∧ ... ∧ am.	
  
	
  onde	
  t1,	
  …,	
  tk	
  são	
  termos	
  e	
  a1,	
  …,	
  am	
  são	
  átomos.	
  
	
  
¨  A	
   desta	
  cláusula	
  de	
  resposta	
  generalizada	
  em	
  ai	
  com	
  
a	
  cláusula	
  
	
  a ← b1 ∧ … ∧ bp. 
	
  no	
  qual	
  ai	
  e	
  a	
  tem	
  como	
  unificador	
  mais	
  geral	
  θ,	
  é	
  
	
  (yes(t1, …,tk) ← 
 a1∧ … ∧ai−1 ∧ b1∧ … ∧bp ∧ ai+1∧ … ∧am)θ. 
Procedimento	
  de	
  prova	
  Top-­‐down	
  
12.4. Proofs and Substitutions 511
1: non-deterministic procedure FODCDeductionTD(KB,q)
2: Inputs
3: KB: a set definite clauses
4: Query q: a set of atoms to prove, with variables V1, . . . ,Vk
5: Output
6: substitution θ if KB |= qθ and fail otherwise
7: Local
8: G is a generalized answer clause
9: Set G to generalized answer clause yes(V1, . . . ,Vk)← q
10: while G is not an answer do
11: Suppose G is yes(t1, . . . , tk)← a1 ∧ a2 ∧ . . . ∧ am
12: select atom ai in the body of G
13: choose clause a← b1 ∧ . . . ∧ bp in KB
14: Rename all variables in a← b1 ∧ . . . ∧ bp to have new names
15: Let σ be unify(ai, a). Fail if unify returns ⊥.
16: assign G the answer clause: (yes(t1, . . . , tk) ← a1 ∧ . . . ∧ ai−1 ∧ b1 ∧
. . . ∧ bp ∧ ai+1 ∧ . . . ∧ am)σ
17: return V1 = t1, . . . ,Vk = tk where G is yes(t1, . . . , tk)←
Figure 12.3: Top-down definite clause proof procedure
Example 12.21 Consider the database of Figure 12.2 (page 505) and the query
ask two doors east(R, r107).
Figure 12.4 (on the next page) shows a successful derivation with answer
R = r111.
Note that this derivation used two instances of the rule
imm east(E,W)← imm west(W,E).
One instance eventually substituted r111 for E, and one instance substituted
r109 for E.
Some choices of which clauses to resolve against may have resulted in a
partial derivation that could not be completed.
Unification
The preceding algorithms assumed that we could find themost general unifier
of two atoms. The problem of unification is the following: given two atoms,
determine if they unify, and, if they do, return an MGU of them.
The unification algorithm is given in Figure 12.5 (page 513). E is a set of
equality statements implying the unification, and S is a set of equalities of the
correct form of a substitution. In this algorithm, if x/y is in the substitution S,
Exemplo:	
  Encadeamento	
  p/	
  trás	
  em	
  LPO	
  
¨  Vamos	
  provar	
  que	
  West	
  é	
  criminoso	
  =	
  criminoso(west).	
  
¨  Inicialmente	
  objeAvos=	
  [criminoso(west)]	
  e	
  θ	
  =	
  {}	
  
¨  criminoso(west) resolve	
  com	
  (1)	
  americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ 
hostil(Z) => criminoso(X),	
  	
  e	
  θ	
  =	
  {X/west}	
  
¤  objeAvos	
  =	
  [americano(west) ٨۸ arma(Y) ٨۸ vende(west,Y,Z) ٨۸ hostil(Z)]	
  
¨  americano(west) resolve	
  com	
  (6)	
  americano(west)‏.	
  
¤  objeAvos	
  =	
  [arma(Y) ٨۸ vende(west,Y,Z) ٨۸ hostil(Z)]	
  
¨  arma(Y) resolve	
  com	
  (4)	
  míssil(X1) => arma(X1)‏ e	
  θ	
  =	
  {X/west,	
  X1/Y}	
  
¤  objeAvos	
  =	
  [missil(Y) ٨۸ vende(west,Y,Z) ٨۸ hostil(Z)]	
  
79 
Exemplo:	
  Encadeamento	
  p/	
  trás	
  em	
  LPO	
  
¨  míssil(Y) resolve	
  com	
  (2)	
  proprietário(nono,m1) ٨۸ míssil(m1)‏ e	
  θ	
  =	
  {X/
west,	
  X1/Y,	
  Y/m1}	
  
¤  objeAvos	
  =	
  [vende(west,m1,Z) ٨۸ hostil(Z)]	
  
¨  vende(west,m1,Z) resolve	
  com	
  	
  (3)	
  míssil(X2) ٨۸ proprietário(nono,X2) => 
vende(west,X2,nono)‏ e	
  θ	
  =	
  {X/west,	
  X1/Y,	
  Y/m1,	
  X2/m1,	
  Z/nono}	
  
¤  objeAvos	
  =	
  [míssil(m1) ٨۸ proprietário(nono,m1) ٨۸ hostil(nono)]	
  
¨  míssil(m1) resolve	
  com	
  (2)	
  proprietário(nono,m1) ٨۸ míssil(m1)‏ 
¤  objeAvos	
  =	
  [proprietário(nono,m1) ٨۸ hostil(Z)]	
  
¨  proprietário(nono,m1) resolve	
  com	
  (2)	
  proprietário(nono,m1) ٨۸ míssil(m1)‏ 
¤  objeAvos	
  =	
  [hostil(nono)]	
  
80 
Exemplo:	
  Encadeamento	
  p/	
  trás	
  em	
  LPO	
  
¨  hostil(mono) resolve	
  com	
  (5)	
  inimigo(X3,américa) => hostil(X3)‏ e	
  θ	
  =	
  {X/
west,	
  X1/Y,	
  Y/m1,	
  X2/m1,	
  Z/nono,	
  X3/nono}	
  
¤  objeAvos	
  =	
  [inimigo(nono,américa)]	
  
¨  inimigo(nono,américa) resolve	
  com	
  (7)	
  inimigo(nono,américa)‏ e	
  θ	
  =	
  {X/
west,	
  X1/Y,	
  Y/m1,	
  X2/m1,	
  Z/nono,	
  X3/Z}	
  
¤  objeAvos	
  =	
  []	
  
81 
Árvore	
  de	
  derivação	
  (top-­‐down)	
  
Hostile(Nono)
Enemy(Nono,America)Owns(Nono,M1)Missile(M1)American(West)
Weapon(M1)
Criminal(West)
Sells(West,M1,Nono)
Exemplo	
  
Example
live(Y )� connected to(Y ,Z ) ⇥ live(Z ). live(outside).
connected to(w6,w5). connected to(w5, outside).
?live(A).
yes(A)� live(A).
yes(A)� connected to(A,Z1) ⇥ live(Z1).
yes(w6)� live(w5).
yes(w6)� connected to(w5,Z2) ⇥ live(Z2).
yes(w6)� live(outside).
yes(w6)� .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.4, Page 14
Exemplo	
  
Example
live(Y )� connected to(Y ,Z ) ⇥ live(Z ). live(outside).
connected to(w6,w5). connected to(w5, outside).
?live(A).
yes(A)� live(A).
yes(A)�connected to(A,Z1) ⇥ live(Z1).
yes(w6)� live(w5).
yes(w6)� connected to(w5,Z2) ⇥ live(Z2).
yes(w6)� live(outside).
yes(w6)� .
c�D. Poole and A. Mackworth 2010 Artificial Intelligence, Lecture 12.4, Page 15
Procedimentos	
  de	
  prova	
  completos	
  
¨  Kurt	
  Gödel	
  (matemáAco	
  alemão)	
  provou	
  os	
  principais	
  teoremas	
  sobre	
  a	
  
completeza	
  dos	
  procedimentos	
  de	
  prova	
  em	
  LPO:	
  
¤  1930	
  -­‐	
  Primeiro	
  teorema	
  da	
  completeza	
  para	
  LPO:	
  qualquer	
  sentença	
  que	
  é	
  
consequência	
  lógica	
  tem	
  uma	
  prova	
  finita.	
   	
  	
  
¤  1931	
  –	
  Teorema	
  da	
  incompletude	
  para	
  LPO:	
  um	
  sistema	
  lógico	
  que	
  inclua	
  o	
  
princípio	
  da	
  indução	
  necessariamente	
  é	
  incompleto.	
  
n  Existem	
  sentenças	
  que	
  são	
  consequências	
  lógicas,	
  mas	
  não	
  têm	
  nenhuma	
  prova	
  
finita	
  dentro	
  sistema.	
  
¨  Apesar	
  do	
  teorema	
  de	
  Gödel,	
  os	
  provadores	
  de	
  teorema	
  baseados	
  em	
  
foram	
  amplamente	
  uAlizados	
  para	
  derivar	
  teoremas	
  
matemáAcos,	
  inclusive	
  alguns	
  que	
  não	
  se	
  conhecia	
  uma	
  prova	
  antes.	
  
Entrada	
  para	
  o	
  algoritmo	
  de	
  resolução	
  
¨  Exige	
  que	
  as	
  sentenças	
  estejam	
  na	
   (uma	
  conjunção	
  de	
  cláusulas	
  em	
  
que	
  cada	
  cláusula	
  é	
  uma	
  disjunção	
  de	
  literais).	
  
¨  Os	
  literais	
  podem	
  conter	
  variáveis,	
  que	
  presumimos	
  ser	
  universalmente	
  
quanAficadas.	
  
¨ 
¨  Exemplo	
  em	
  LPO:	
  
∀X americano(X) ٨۸ arma(Y) ٨۸ vende(X,Y,Z) ٨۸ hostil(Z) => criminoso(X)‏ 
¨  ConverAda	
  para	
  FNC:	
  
¬americano(X) ٧۷ ¬arma(Y) ٧۷ ¬vende(X,Y,Z) ٧۷ ¬hostil(Z) ٧۷ criminoso(X)‏ 
Conversão	
  para	
  FNC	
  
¨  É	
  bem	
  parecida	
  com	
  a	
  conversão	
  em	
  LP,	
  exceto	
  pela	
  necessidade	
  de	
  
eliminar	
  os	
  quanAficadores	
  existenciais.	
  
¨  Exemplo:	
  “Todo	
  mundo	
  que	
  ama	
  todos	
  os	
  animais	
  é	
  amado	
  por	
  alguém”.	
  
	
  ∀X [∀Y animal(Y) => ama(X,Y)] => [∃Y ama(Y,X)] 
¨  Etapas	
  da	
  conversão:	
  
¤  :	
  
 ∀X [¬∀Y ¬animal(Y) V ama(X,Y)] V [∃Y ama(Y,X)] 
¤  :	
  
n  Precisaremos,	
  além	
  das	
  regras	
  habituais,	
  também	
  das	
  regras	
  para	
  quanAficadores	
  
negados:	
  
 ¬∀X p torna-­‐se	
  ∃X ¬p 
 ¬∃X p torna-­‐se	
  ∀X ¬p 
Conversão	
  para	
  FNC	
  
¨  :	
  
∀X [¬∀Y ¬animal(Y) V ama(X,Y)] V [∃Y ama(Y,X)] 
∀X [∃Y ¬(¬animal(Y) V ama(X,Y))] V [∃Y ama(Y,X)] 
∀X [∃Y animal(Y) ٨۸ ¬ama(X,Y)] V [∃Y ama(Y,X)]	
  
¨  :	
  
∀X [∃Y animal(Y) ٨۸ ¬ama(X,Y)] V [∃Z ama(Z,X)] 
¨  :	
  É	
  o	
  processo	
  de	
  remover	
  quanAficadores	
  existenciais	
  por	
  
eliminação.	
  No	
  caso	
  simples,	
  é	
  idênAca	
  à	
  regra	
  de	
  instanciação	
  do	
  
existencial.	
  
∀X [animal(a) ٨۸ ¬ama(X,a)] V [ama(b,X)] 
 
¤  “Todo	
  mundo	
  deixa	
  de	
  amar	
  uma	
  animal	
  A	
  específico,	
  ou	
  é	
  amado	
  por	
  alguma	
  
enAdade	
  específica	
  B”	
  
Conversão	
  para	
  FNC	
  
¨  :	
  Queremos	
  que	
  as	
  enAdades	
  de	
  Skolem	
  dependam	
  de	
  X.	
  
∀X [animal(f(X)) ٨۸ ¬ama(X,f(X))] V [ama(g(X),X)] 
¤  f(X) e	
  g(X) são	
   .	
  Os	
  argumentos	
  da	
  função	
  de	
  Skolem	
  são	
  
todas	
  as	
  variáveis	
  universalmente	
  quan5ficadas,	
  em	
  cujo	
  escopo	
  aparece	
  o	
  
quanAficador	
  existencial.	
  
¨  :	
  
[animal(f(X)) ٨۸ ¬ama(X,f(X))] V [ama(g(X),X)] 
¨  :	
  
[animal(f(X)) V ama(g(X),X)] ٨۸ [¬ama(X,f(X)) V ama(g(X),X)] 
¤  f(X) –	
  se	
  refere	
  ao	
  animal	
  potencialmente	
  não	
  amado	
  por	
  X.	
  
¤  g(X) –	
  se	
  refere	
  a	
  alguém	
  que	
  poderia	
  amar	
  X.	
  
A	
  regra	
  de	
  inferência	
  de	
  resolução	
  
¨  Duas	
  cláusulas	
  podem	
  ser	
  resolvidas	
  se	
  contém	
  literais	
  complementares.	
  
¤  Literais	
  de	
  primeira	
  ordem	
  são	
  complementares	
  se	
  um	
  deles	
  se	
   	
  com	
  a	
  
negação	
  do	
  outro.	
  
:	
  
 α1٧۷...٧۷ αk, β1٧۷...٧۷ βn 
 SUBST(θ, α1٧۷...٧۷ αi-1 ٧۷ αi+1٧۷...٧۷ αk ٧۷ β1٧۷...٧۷ βj-1 ٧۷ βj+1٧۷...٧۷ βn)‏ 
	
  onde	
  UNIFICA(αi,	
  βj)=θ.	
  
¨  Exemplo:	
  
 [animal(f(X)) V ama(g(X),X)], [¬ama(U,W) V ¬mata(U,W)] 
 [animal(f(X)) V ¬mata(g(X),X)] 
	
  
	
  com	
  UNIFICA(U/g(X),	
  W/X)=θ.	
  
Regra	
  de	
  Resolução	
  +	
  Fatoração	
  
¨  A	
  regra	
  de	
  resolução	
  binária	
  sozinha	
  não	
  gera	
  um	
  
procedimento	
  de	
  inferência	
  completo.	
  
¨  A	
  regra	
  de	
  resolução	
  +	
  fatoração	
  é	
  um	
  procedimento	
  de	
  
inferência	
  completo.	
  
¤  Fatoração	
  proposicional	
  –	
  reduz	
  dois	
  literais	
  a	
  um	
  só	
  se	
  eles	
  são	
  
.	
  
¤  Fatoração	
  de	
  primeira	
  ordem	
  –	
  reduz	
  dois	
  literais	
  a	
  um	
  só	
  se	
  eles	
  são	
  
.	
  
n  O	
  unificador	
  deve	
  ser	
  aplicado	
  à	
  cláusula	
  inteira.	
  
Exemplo	
  de	
  prova	
  por	
  resolução	
  
¨  As	
  sentenças	
  do	
  exemplo	
  do	
  crime	
  em	
  FNC:	
  
(1) ¬americano(X) V ¬arma(Y) V ¬vende(X,Y,Z) V ¬hostil(Z) V criminoso(X)‏ 
(2a) proprietário(nono, M1)‏ 
(2b) míssil(M1)‏ 
(3) ¬míssil(x) V ¬proprietário(nono, x) V vende(west,x,nono)‏ 
(4) ¬míssil(x) V Arma(x)‏ 
(5) ¬inimigo(x,américa) V hostil(X)‏ 
(6) americano(west)‏ 
(7) inimigo(nono,américa)‏ 
¨  Queremos	
  provar:	
  criminoso(west)‏ 
Árvore	
  de	
  derivação	
  (resolução)	
  
¬American(x) ¬Weapon(y) ¬Sells(x,y,z) ¬Hostile(z) Criminal(x) ¬Criminal(West)
¬Enemy(Nono, America)Enemy(Nono,America)
¬Missile(x) Weapon(x) ¬Weapon(y) ¬Sells(West,y,z) ¬Hostile(z)
Missile(M1) ¬Missile(y) ¬Sells(West,y,z) ¬Hostile(z)
¬Missile(x) ¬Owns(Nono,x) Sells(West,x,Nono) ¬Sells(West,M1,z) ¬Hostile(z)
¬American(West) ¬Weapon(y) ¬Sells(West,y,z) ¬Hostile(z)American(West)
¬Missile(M1) ¬Owns(Nono,M1) ¬Hostile(Nono)Missile(M1)
¬Owns(Nono,M1) ¬Hostile(Nono)Owns(Nono,M1)
¬Enemy(x,America) Hostile(x) ¬Hostile(Nono)
^
^^
^
^
^
^
^
^ ^
^
^
^
^
^
^
^
^
^
Prova	
  por	
  resolução	
  e	
  ET	
  
¨  A	
  coluna	
  em	
  cinza	
  começa	
  com	
  a	
  cláusula	
  objeAvo,	
  
resolvendo	
  cláusulas	
  desde	
  a	
  BC	
  até	
  a	
  cláusula	
  vazia.	
  
¤  CaracterísAca	
  da	
  resolução	
  sobre	
  BC	
  de	
  cláusulas	
  de	
  Horn.	
  
¤  As	
  cláusulas	
  ao	
  longo	
  da	
  coluna	
  principal	
  correspondem	
  exatamente	
  
aos	
  valores	
  sucessivos	
  da	
  variável	
  objeAvos	
  no	
  algoritmo	
  de	
  ET.	
  
¨  O	
  encadeamento	
  para	
  trás	
  é	
  realmente	
  apenas	
  um	
  caso	
  
especial	
  de	
  resolução	
  com	
  uma	
  estratégia	
  de	
  controle	
  
específica	
  para	
  decidir	
  que	
  resolução	
  executar	
  em	
  seguida.	
  
Exemplo	
  com	
  cláusulas	
  que	
  não	
  são	
  
definidas	
  e	
  skolemização	
  
¨  O	
  problema	
  em	
  linguagem	
  natural:	
  
¤  Todo	
  mundo	
  que	
  ama	
  todos	
  os	
  animais	
  é	
  amado	
  por	
  alguém.	
  
¤  Qualquer	
  um	
  que	
  mata	
  um	
  animal	
  é	
  amadopor	
  ninguém.	
  
¤  João	
  ama	
  todos	
  os	
  animais.	
  
¤  João	
  ou	
  a	
  Curiosidade	
  matou	
  o	
  gato,	
  que	
  se	
  chama	
  Atum.	
  
¤  A	
  Curiosidade	
  matou	
  o	
  gato?	
  
Exemplo	
  com	
  cláusulas	
  que	
  não	
  são	
  
definidas	
  e	
  skolemização	
  
¨  O	
  problema	
  em	
  LPO:	
  
1.  ∀X [∀Y animal(Y) => ama(X,Y)] => [∃Y ama(Y,X)] 
2.  ∀X [∃Y animal(Y) ٨۸ mata(X,Y)] => [∀z ¬ama(Z,X)] 
3.  ∀X animal(X) => ama(joão,X)‏ 
4.  mata(joão,atum) V mata(curiosidade,atum)‏ 
5.  gato(atum)‏ 
6.  ∀X gato(X) ٨۸ animal(X)‏ 
7.  ¬mata(curiosidade,atum)‏ 
Exemplo	
  com	
  cláusulas	
  que	
  não	
  são	
  
definidas	
  e	
  skolemização	
  
¨  O	
  problema	
  em	
  FNC:	
  
1.  animal(f(X)) V ama(g(X),X)‏ 
2.  ¬ama(x,f(X)) V ama(f(X),X)‏ 
3.  ¬animal(Y) V ¬mata(X,Y) V ¬ama(Z,X)‏ 
4.  ¬animal(x) V ama(joão,X)‏ 
5.  mata(joão,atum) V mata(curiosidade,atum)‏ 
6.  gato(atum)‏ 
7.  ¬gato(X) V animal(X)‏ 
8.  ¬mata(curiosidade,atum)‏ 
Àrvore	
  de	
  derivação	
  (resolução)	
  
¬Loves(y, Jack) Loves(G(Jack), Jack)
¬Kills(Curiosity, Tuna)Kills(Jack, Tuna) Kills(Curiosity, Tuna)¬Cat(x) Animal(x)Cat(Tuna)
¬Animal(F(Jack)) Loves(G(Jack), Jack) Animal(F(x)) Loves(G(x), x) ¬Loves(y, x) ¬Kills(x, Tuna)
Kills(Jack, Tuna)¬Loves(y, x) ¬Animal(z) ¬Kills(x, z)Animal(Tuna) ¬Loves(x,F(x)) Loves(G(x), x) ¬Animal(x) Loves(Jack, x)
^
^
^
^
^ ^
^^^
Estratégias	
  de	
  Resolução	
  
¨  Aplicações	
  repeAdas	
  da	
  regra	
  de	
  inferência	
  de	
  resolução	
  
eventualmente	
  encontrarão	
  uma	
  prova,	
  se	
  exisAr	
  alguma.	
  
¨  Algumas	
  estratégias	
  ajudam	
  a	
  encontrar	
  prova	
  de	
  maneira	
  
eficiente.	
  
¤  Preferência	
  unitária	
  
¤  Conjunto	
  de	
  suporte	
  
¤  Resolução	
  de	
  entrada	
  
¤  Subordinação	
  
Preferência	
  Unitária	
  
¨  Dá	
  preferência	
  a	
  resoluções	
  em	
  que	
  uma	
  das	
  sentenças	
  é	
  um	
  
único	
  literal.	
  
¨  Estamos	
  tentando	
  produzir	
  uma	
  cláusula	
  vazia	
  e,	
  assim,	
  pode	
  
ser	
  uma	
  boa	
  ideia	
  produzir	
  cláusulas	
  cada	
  vez	
  mais	
  curtas.	
  
¨  A	
   é	
  uma	
  forma	
  restrita	
  de	
  resolução,	
  na	
  
qual	
  toda	
  etapa	
  de	
  resolução	
  deve	
  envolver	
  uma	
  cláusula	
  
unitária.	
  
¤  É	
  incompleta	
  no	
  caso	
  geral,	
  mas	
  é	
  completa	
  para	
  BC	
  na	
  forma	
  de	
  
cláusulas	
  de	
  Horn.	
  
Conjunto	
  de	
  Suporte	
  
¨  Começa	
  idenAficando	
  um	
  conjunto	
  de	
  sentenças	
  chamado	
  conjunto	
  de	
  
suporte.	
  
¤  Uma	
  abordagem	
  comum	
  é	
  usar	
  a	
  consulta	
  negada	
  como	
  conjunto	
  de	
  suporte.	
  
¨  Toda	
  resolução	
  combina	
  uma	
  sentença	
  do	
  conjunto	
  de	
  suporte	
  com	
  outra	
  
sentença	
  e	
  adiciona	
  o	
  resolvente	
  ao	
  conjunto	
  de	
  suporte.	
  
¨  Se	
  o	
  conjunto	
  de	
  suporte	
  for	
  pequeno	
  em	
  relação	
  à	
  BC	
  inteira,	
  o	
  espaço	
  
de	
  busca	
  será	
  drasAcamente	
  reduzido.	
  
¨  Se	
  escolhermos	
  o	
  conjunto	
  de	
  suporte	
  de	
  forma	
  que	
  as	
  sentenças	
  
restantes	
  sejam	
  saAsfazíveis	
  em	
  conjunto,	
  então	
  a	
  resolução	
  pelo	
  
conjunto	
  de	
  suporte	
  será	
  completa.	
  
¤  O	
  uso	
  da	
  consulta	
  negada	
  como	
  conjunto	
  de	
  suporte	
  supõe	
  que	
  a	
  BC	
  original	
  é	
  
consistente.	
  
Resolução	
  de	
  entrada	
  
¨  Toda	
  resolução	
  combina	
  uma	
  das	
  sentenças	
  de	
  entrada	
  (da	
  
BC	
  ou	
  da	
  consulta)	
  com	
  alguma	
  outra	
  sentença	
  (produzida	
  
pela	
  resolução).	
  
¤  Como	
  o	
  a	
  prova	
  por	
  resolução	
  do	
  exemplo	
  do	
  crime.	
  
¨  Em	
  BCs	
  de	
  Horn,	
  o	
  Modus	
  Ponens	
  é	
  uma	
  espécie	
  de	
  
estratégia	
  de	
  resolução	
  de	
  entrada.	
  
¤  Por	
  isso,	
  a	
  resolução	
  de	
  entrada	
  é	
  completa	
  para	
  BCs	
  de	
  Horn,	
  mas	
  é	
  
incompleta	
  no	
  caso	
  geral.	
  
Subordinação	
  
¨  Elimina	
  todas	
  as	
  sentenças	
  que	
  são	
  subordinadas	
  por	
  uma	
  
sentença	
  existente	
  na	
  BC	
  (isto	
  é,	
  são	
  mais	
  específicas).	
  
¤  Exemplo:	
  	
  
n  Se	
  p(X)	
  está	
  na	
  BC,	
  então	
  não	
  faz	
  senAdo	
  adicionar	
  p(a)	
  ou	
  p(a)	
  V	
  q(b).	
  
¨  Isto	
  ajuda	
  a	
  manter	
  a	
  BC	
  pequena,	
  e	
  isso	
  ajuda	
  a	
  manter	
  o	
  
espaço	
  de	
  busca	
  pequeno.