Upload
buidung
View
226
Download
0
Embed Size (px)
Citation preview
Sumário
• Inferência em lógica proposicional vs. inferência em lógica de primeira ordem
• Unificação
• Modus Ponens Generalizado
• Encadeamento para a frente
• Encadeamento para trás
• Resolução
Instanciação Universal
• A partir de uma frase com um quantificador universal, podemos inferir uma frase que resulta da substituição da variável por um termo sem variáveis
v αSubst({v/g}, α)
• E.g., x Rei(x) Ambicioso(x) Malvado(x) permite inferir:Rei(João) Ambicioso(João) Malvado(João)
Rei(Ricardo) Ambicioso(Ricardo) Malvado(Ricardo)
Rei(Pai(João)) Ambicioso(Pai(João)) Malvado(Pai(João))
.
.
.
Instanciação Existencial
• Para uma frase α, uma variável v, e uma constante k que não aparece em nenhuma frase da base de conhecimento
v αSubst({v/k}, α)
• E.g., A partir de x ECoroa(x) NaCabeca(x,João) podemos inferir ECoroa(C1) NaCabeca(C1,João)
desde que C1 seja um símbolo de constante novo, chamado constante de Skolem
• A frase que contém o quantificador existencial pode ser eliminada equivalência por inferência
Redução para inferência proposicional
Consideremos que a BC contém as seguintes frases:x Rei(x) Ambicioso(x) Malvado(x)Rei(João)Ambicioso(João)Irmãos(Ricardo,João)
• Instanciando a frase com de todas as formas possíveis, obtemos:Rei(João) Ambicioso(João) Malvado(João)Rei(Ricardo) Ambicioso(Ricardo) Malvado(Ricardo)Rei(João)Ambicioso(João)Irmãos(Ricardo,João)
• A BC está proposicionalizada, ou seja, contém apenas símbolos proposicionais:
Rei(João), Ambicioso(João), Malvado(João), Rei(Ricardo), etc.
Redução (cont.)
• Todas as BC em LPO podem ser proposicionalizadas de modo a preservar as consequências lógicas
• Uma termo sem variáveis é consequência da nova BC sse é consequência lógica da BC original
• Ideia: proposicionalizar BC e frase que é consequência lógica – aplicar resolução para fazer a prova
• Problema: para símbolos de função o número de termos sem variáveis é infinito– e.g., Pai(Pai(Pai(João)))
Redução (cont.)
Teorema [Herbrand,1930] Se uma frase α é consequência lógica de uma BC em LPO, então α é consequência lógica de um subconjunto finito da BC proposicionalizada
Ideia: Para n = 0 ∞criar uma BC proposicional instanciando termos até à profundidade n verificar se α é consequência lógica da BC
Problema: funciona se α é efectivamente consequência lógica, não termina se α não é consequência lógica
Teorema [Turing,1936][Church,1936] Consequências lógicas em LPO são semi-decidíveis, i.e. existem algoritmos que identificam consequências lógicas, mas não existem algoritmos que identifiquem frases que não são consequências lógicas
Proposicionalização: problemas• Proposicionalização pode gerar muitas frases irrelevantes
• E.g., a partir de:x Rei(x) Ambicioso(x) Malvado(x)Rei(João)y Ambicioso(y)Irmãos(Ricardo,João)
• Parece óbvio inferir Malvado(João), mas a proposicionalizaçãoproduz outros factos como Ambicioso(Ricardo) que são irrelevantes
• Para p predicados com aridade k e n constantes, existem p·nk
instanciações possíveis
Unificação
x Rei(x) Ambicioso(x) Malvado(x)• Se conseguimos encontrar uma substituição θ para x para a qual se
verifica Rei(x) e Ambicioso(x) então podemos inferir Malvado(x)• Genericamente: se conseguirmos encontrar uma substituição θ que
converta a premissa de uma implicação numa frase já existente na BC, então podemos derivar a conclusão da implicação após efectuada a substituição θ
Exº• x Rei(x) Ambicioso(x) Malvado(x)• Rei(João)• y Ambicioso(y)θ = {x/João,y/João} permite inferir Malvado(João)
• Unificação = identificação de uma substituição que permita que duas frases sejam logicamente equivalentes
Unificação: exemplo
• Unificação(α,β) = θ se αθ = βθ
α β θConhece(João,x) Conhece(João,Rita) Conhece(João,x) Conhece(y,Isabel) Conhece(João,x) Conhece(y,Mãe(y))Conhece(João,x) Conhece(x,Isabel)
Unificação: exemplo
• Unificação(α,β) = θ se αθ = βθ
α β θConhece(João,x) Conhece(João,Rita) {x/Rita}Conhece(João,x) Conhece(y,Isabel) Conhece(João,x) Conhece(y,Mãe(y))Conhece(João,x) Conhece(x,Isabel)
Unificação: exemplo
• Unificação(α,β) = θ se αθ = βθ
α β θConhece(João,x) Conhece(João,Rita) {x/Rita}Conhece(João,x) Conhece(y,Isabel) {x/Isabel,y/João}Conhece(João,x) Conhece(y,Mãe(y))Conhece(João,x) Conhece(x,Isabel)
Unificação: exemplo
• Unificação(α,β) = θ se αθ = βθ
α β θConhece(João,x) Conhece(João,Rita) {x/Rita}Conhece(João,x) Conhece(y,Isabel) {x/Isabel,y/João}Conhece(João,x) Conhece(y,Mãe(y)) {y/João,x/Mãe(João)}Conhece(João,x) Conhece(x,Isabel)
Unificação: exemplo
• Unificação(α,β) = θ se αθ = βθ
α β θConhece(João,x) Conhece(João,Rita) {x/Rita}Conhece(João,x) Conhece(y,Isabel) {x/Isabel,y/João}Conhece(João,x) Conhece(y,Mãe(y)) {y/João,x/Mãe(João)}Conhece(João,x) Conhece(x,Isabel) {falha}
Estandardização
• Conhece(João,x) e Conhece(x,Isabel) poderão ser unificados se substituirmos x por outra variável
• Esta unificação faz sentido– Conhece(João,x) significa que o João conhece toda a gente– Conhece(x,Isabel) significa que a Isabel é conhecida por toda a
gente– Logo, o João conhece a Isabel
• Estandardização = renomeação de variáveis numa das duas frases a serem unificadas para evitar conflitos nos nomes das variáveis
• Conhece(João,x) e Conhece(y,Isabel) pode ser unificado com {x/Isabel,y/João}
Unificação: UMG
• Para unificar Conhece(João,x) e Conhece(y,z),θ = {y/João, x/z } ou θ = {y/João, x/João, z/João}
• A primeira substituição é mais genérica do que a segunda.
• Existe um único unificador mais geral (UMG): efectua o menor número de substituições para unificar dois termosUMG = { y/João, x/z }
Algoritmo de UnificaçãoFunção Unifica(x,y,) devolve uma substituição que unifica x e y
(x e y são variáveis, constantes, compostos ou listas, inicialmente vazio)se =falha então devolve falhasenão se x=y então devolve senão se Variável?(x) então devolve UnificaVar(x,y,)senão se Variável?(y) então devolve UnificaVar(y,x,)senão se Composto?(x) e Composto?(y) então
devolve Unifica(Args[x],Args[y],Unifica(Op[x],Op[y],))senão se Lista?(x) e Lista?(y) então
devolve Unifica(Rest[x],Rest[y],Unifica(First[x],First[y],))senão devolve falha
Exº para o composto F(A,B) temos Op[F(A,B)]=F e Args[F(A,B)]=(A,B)
Algoritmo de UnificaçãoFunção UnificaVar(var,x,) devolve uma substuição
(x é uma expressão)
se {var/val} então devolve Unifica(val,x,)senão se {x/val} então devolve Unifica(var,val,)senão se VerificaOcorrencia?(var,x) então devolve falhasenão adiciona {var/x} a
VerificaOcorrencia?(var,x) verifica se var ocorre na expressão x
Complexidade do algoritmo é quadrática na dimensão das expressões que pretendemos unificar
Modus Ponens Generalizado (MPG)
p1', p2', … , pn', ( p1 p2 … pn q)qθ
p1' é Rei(João) p1 é Rei(x) p2' é Ambicioso(y) p2 é Ambicioso(x) θ é {x/João,y/João} q é Malvado(x) q θ é Malvado(João)
• MPG usado com BC com cláusulas que têm exactamente um literal positivo: (p1 p2 … pn q) equivale a (p1 p2 … pn q)
• Todas as variáveis estão quantificadas universalmente
com pi'θ = pi θ para todo o i
Solidez de MPG
• É preciso provar quep1', …, pn', (p1 … pn q) ╞ qθ
quando temos pi'θ = piθ para todo o i
• Lema: Para qualquer frase p, temos p ╞ pθ pela instanciação universal
1. (p1 … pn q) ╞ (p1 … pn q)θ = (p1θ … pnθ qθ)2. p1', … ,pn' ╞ p1' … pn' ╞ p1'θ … pn'θ3. A partir de 1 e 2 obtemos qθ por Modus Ponens
Exemplo: base de conhecimento
• Do ponto de vista legal, um Americano é um criminoso por vender armas a nações hostis. O país Nono, um inimigo da América, possui alguns mísseis, e todos estes mísseis foram-lhe vendidos pelo Coronel West, que é Americano.
• Objectivo: provar que o Coronel West é um criminoso.
Exemplo: base de conhecimento (cont.)
... um Americano é um criminoso por vender armas a nações hostis:Americano(x) Arma(y) Vende(x,y,z) Hostil(z) Criminoso(x)
Nono … possui alguns mísseis, i.e., x Possui(Nono,x) Míssil(x):Possui(Nono,M1) e Missil(M1) [instanciação existencial]
… todos os mísseis foram-lhe vendidos pelo Coronel WestMissil(x) Possui(Nono,x) Vende(West,x,Nono)
Mísseis são armas:Missil(x) Arma(x)
Um inimigo da América é considerado “hostil”:Inimigo(x,America) Hostil(x)
West é Americano …Americano(West)
O país Nono é um inimigo da América …Inimigo(Nono,America)
Encadeamento progressivo: algoritmo
Função EP-LPO-Pergunta(BC,) devolve uma substuição ou falso(var.local) novo conjº de frases inferidas em cada iteraçãorepetir até novo ser vazio
novo { }paracada frase r na BC
(p1 … pn q) estandardização(r)paracada t.q. (p1 … pn q) = (p1‘ … pn‘ q)
para algum p1‘, …, pn‘ na BCq’ qse q’ não é uma renomeação de uma frase na BC
ou em novo entãoadicionar q’ a novo Unifica(q’,)se não é falha então devolve
adiciona novo à BCdevolve falso
Exº de renomeação: Gosta(x,Gelado) e Gosta(y,Gelado)
Propriedades do encadeamento progressivo
• Sólido e completo para cláusulas na forma (p1 … pn q) em lógica de primeira ordem
• Datalog = cláusulas na forma (p1 … pn q) em lógica de primeira ordem + não há funções
• EP termina para Datalog num número finito de iterações
• Não termina se α não é consequência lógica
• Não podemos resolver este problema: encadeamento progressivo é semi-decidível
Eficiência do encadeamento progressivo
Encadeamento progressivo incremental: só é necessário fazer um emparelhamento de uma frase na iteração k se uma premissa tiver sido adicionada na iteração k-1 Emparelhar cada frase cuja premissa contém um novo literal
positivo
Emparelhamento pode ser dispendioso:Bases de dados indexadas permitem encontrar factos
conhecidos em tempo constante (O(1))– e.g., pergunta Missil(x) responde Missil(M1)
Encadeamento progressivo é muito usado em bases de dados dedutivas
Emparelhamento: exemplo
Míssil(x) Possui(Nono,x) Vende(West,x,Nono)
• Podemos obter os objectos possuídos pelo Nono em tempo constante, e depois verificar se algum desses objectos é um míssil
• Se existirem muitos objectos possuídos pelo Nono e poucos mísseis, então é preferível começar por obter os mísseis e posteriormente verificar quais são possuídos pelo Nono
Emparelhamento difícil: exemplo
• ColoracaoOK() é inferido sse o CSP tem solução• Dificilmente conseguimos perceber qual a ordem a
seguir para fazer o emparelhamento de menor custo
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) ColoracaoOK()
Diff(Verm,Azul) Diff (Verm,Verde) Diff(Verde,Verm) Diff(Verde,Azul) Diff(Azul,Verm) Diff(Azul,Verde)
Emparelhamento difícil: soluções
• Objectivo: encontrar uma ordenação óptima de modo a que o custo do emparelhamento seja minimizado NP-difícil para problemas NP-difíceis!
• Solução: uso de heurísticas; e.g. escolher variável com mais restrições
Encadeamento regressivo: algoritmo
SUBST(COMPOE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p))
Função ER-LPO-Pergunta(BC,objectivos,)devolve conjunto de substituições
, substituição actual, inicialmente { }(var.local) resp, conjº de substituições, inicialmente { }
se objectivos está vazio então devolver {}q’ Substitui(,First(objectivos))paracada r em BC onde estandardização(r) = (p1 … pn q)
e ’ Unifica(q,q’) não falharesp ER-LPO-Pergunta(BC,[p1,…,pn|Rest(objectivos)],
COMPOE(, ’)) respdevolve resp
Propriedades do encadeamento regressivo
• Prova com procura em profundidade com recursão: espaço é linear no tamanho da prova
• Incompletude devido a ciclos infinitos– Podem ser evitados comparando o objectivo actual
com os objectivos na pilha
• Ineficiente devido à existência de sub-objectivos repetidos (tanto com sucesso como falha)– Guardar em memória resultados obtidos
anteriormente memória adicional
• Muito usado em programação em lógica
Programação em Lógica: Prolog
• Algoritmo = Lógica + Controlo
• Base: encadeamento regressivo com cláusulas de HornFácil prototipagem, manipulação de símbolos (e.g. compiladores, parsing de língua natural)
• Programa = conjunto de cláusulas = cabeça :- literal1, … literaln.criminoso(X) :- americano(X), arma(Y), vende(X,Y,Z), hostil(Z).
• Encadeamento regressivo: profundidade, esquerdadireita• Predicados pré-definidos para aritmética etc., e.g., X is Y*Z+3.• Predicados pré-definidos com efeitos colaterais• Mundo fechado
– e.g., considerando vivo(X) :- not morto(X).– vivo(joão) é verdade se morto(joao) falha
Prolog (1)
• Concatenação de duas listas para produzir uma terceira lista:append([],Y,Y).
append([A|X],Y,[A|Z]) :- append(X,Y,Z).
• Aparentemente semelhante à definição de Lisp mas com mais funcionalidades
• Questão: append(A,B,[1,2]) ?
• Respostas: A=[] B=[1,2]A=[1] B=[2]
A=[1,2] B=[]
Prolog: appendProcedimento Append(ax,y,az)
caminho ApontadorGlobalCaminho()se ax=[] e Unifica(y,az) então continuaResetCaminho(caminho)a NovaVariavel(), x NovaVariavel(), z NovaVariavel()se Unifica(ax,[a|x]) e unifica(az,[a|z]) então Append(x,y,z)
Prolog(2)
• Definição de caminho entre dois pontos:path(X,Z): link(X,Z).path(X,Z): path(X,Y),link(Y,Z).path(X,Z): link(X,Y),path(Y,Z).
• Ordem é relevante!
descendente(D,A):-progenitor(A,D). descendente(D,A):-
progenitor(P,D),descendente(P,A).
fact(0,1).fact(N,F):- N>0, N1 is N-1, fact(N1,F1),
F is N*F1.
Prolog(3)
soma(0,X,X). % 0+X=Xsoma(s(X),Y,Z) :- soma(X,s(Y),Z).
% (X+1)+Y=Z <== X+(Y+1)=Z
?- soma(s(s(s(0))),s(0),Total).?- soma(s(s(0)),s(s(0)),Total).?- soma(s(0),s(s(s(0))),Total). ?- soma(0,s(s(s(s(0)))),Total). Total=s(s(s(s(0))))
Resolução em LPO
l1 ··· lk, m1 ··· mn
(l1 ··· li-1 li+1 ··· lk m1 ··· mj-1 mj+1 ··· mn)θcom Unifica(li, mj) = θ.
• Aplica-se a fórmulas no formato CNF• Por exemplo,
Rico(x) Infeliz(x) Rico(João)
Infeliz(João)com θ = {x/João}
• Assume-se que as duas cláusulas estão estandardizadas não têm variáveis em comum
CNF para LPO
1. Eliminação de e 2. Leis de DeMorgan
3. Estandardização de variáveis
4. Skolemização
5. Eliminação de quantificadores universais
6. Distributividade de sobre
Skolemização
• Consiste na remoção de quantificadores existenciais por eliminação
• Caso simples: substituir x P(x) por P(A) em que A é uma constante de Skolem (constante nova, nunca usada anteriormente)
• Caso complexo: quando existem quantificadores encadeados xy P(x,y) substituído por x P(x,F(x)) em que F é uma função de Skolem– Caso geral: argumentos da função de Skolem são
todas as variáveis quantificadas universalmente que aparecem antes do quantificador existencial
CNF para LPO: exemploAs pessoas que gostam de todos os animais têm alguém que gosta delas.
x [y Animal(y) Gosta(x,y)] [y Gosta(y,x)]
x [y Animal(y) Gosta(x,y)] [y Gosta(y,x)]
x [y Animal(y) Gosta(x,y)] [y Gosta(y,x)]
x [y Animal(y) Gosta(x,y)] [y Gosta(y,x)]
x [y Animal(y) Gosta(x,y)] [y Gosta(y,x)]
x [y Animal(y) Gosta(x,y)] [z Gosta(z,x)]
x (Animal(F(x)) Gosta(x,F(x))) Gosta(G(x),x)
(Animal(F(x)) Gosta(x,F(x))) Gosta(G(x),x)
Animal(F(x)) Gosta(G(x),x)
Gosta(x,F(x)) Gosta(G(x),x)
Resolução em LPO: completude
• Resolução binária aplica-se exactamente a 2 literais; não é suficiente para garantir completude
• Factorização = remoção de literais redundantes– Em lógica proposicional = remoção de literais
repetidos
– Em lógica de primeira ordem = remoção de literais unificáveis!
• Resolução binária + factorização completude
Resolução: completude por refutação
• Se um conjunto de frases não tem solução, então tem de ser possível derivar uma contradição (cláusula vazia, ()) por resolução
• Ver prova no Livro
Igualdade
• Nenhum dos métodos de inferência anteriores lida com igualdade
• Possível solução adicionar axiomas de igualdade: reflexiva, simétrica, transitiva, substituição– x x=x– x,y x=y y=x– x,y,z x=y y=z x=z– x,y x=y (P(x)P(y))– …
• Outras técnicas: demodulação, paramodulação
Estratégias para Resolução (1)
• Preferência pela cláusula unitária– Aplicar resolução em que uma das cláusulas é
unitária nova cláusula com dimensão mais reduzida
• Conjunto de suporte– Conjunto de suporte = subconjunto de cláusulas– Cada resolução combina uma cláusula do conjunto
de suporte com outra cláusula e adiciona a cláusula resultante ao conjunto de suporte
– Se o conjunto de suporte é pequeno o espaço de procura pode ficar bastante reduzido
– Exº usar frase negada como conjunto de suporte resolução orientada ao objectivo
Estratégias para Resolução (2)
• Resolução pela entrada– Cada passo de resolução utiliza uma cláusula
acabada de gerar
– Estratégia completa para cláusulas de Horn mas não completa para o caso geral
• Eliminação de cláusulas– Cláusulas eliminadas devido à existência de
cláusulas mais genéricas
– Exº P(A) é redundante vs. P(x)
– Exº P(A)P(B) é redundante vs. P(A)