[figure]

Lógica de Primeira Ordem

• necessário: regras para dizer se o mundo continuou o mesmo.

• ∀a, x, s Holding(x, s) ∧ (a ≠ Release) ⇒ Holding(x, Result(a, s))

• ∀a, x, s ¬Holding(x, s) ∧ (a ≠ Grab ∨ ¬(P resent(x, s) ∧ P ortable(x)) ⇒ ¬Holding(x, Result(a, s))

• axiomas de frame.

• combinação de axiomas de efeito e de frame:

verdadeiro posteriormente

⇔ [uma ação fez ser verdadeiro ∨ já era verdadeiro antes]

Lógica de Primeira Ordem

• ∀a, s, x Holding(x, Result(a, s)) ⇔ [(a = Grab ∧ P resent(x, s) ∧ P ortable(x)) ∨ (Holding(x, s) ∧ a ≠ Release)]

• axioma do estado sucessor.

• necessário para cada predicado que pode mudar seu valor no decorrer do tempo.

[figure]

Lógica de Primeira Ordem

• Localização do agente.

– qual é a sua direção: N, S, O, L? Convenção: 0 degrees anda p/ direita ou esquerda, 90 degrees anda p/ baixo ou p/ cima. Ex: Orientation(Agent, S_{0}) = 0

– Como as posições são mapeadas?

∗ ∀x, y LocationT oward([x, y], 0) = [x + 1, y]

∗ ∀x, y LocationT oward([x, y], 90) = [x, y + 1]

∗ ∀x, y LocationT oward([x, y], 180) = [x − 1, y]

∗ ∀x, y LocationT oward([x, y], 270) = [x, y − 1]

∗ do mapa é possível dizer se um quadrado está diretamente a frente do agente: · ∀p, l, s At(p, l, s) ⇒ LocationAhead(p, s) = LocationT oward(l, Orientation(p, s)) · adjacência: ∀l_{1}, l_{2} Adj(l_{1}, l_{2}) ⇔ ∃dl_{1} = LocationT oward(l_{2}, d)

[figure]

Lógica de Primeira Ordem

• O que as ações devem fazer com as posições?

– ∀a, d, p, s At(p, l, Result(a, s)) = d ⇔ [(a = F orward ∧ l = LocationAhead(p, s) ∧ ¬W all(l)) ∨ (At(p, l, s) ∧ a ≠ F orward)]

• O que as ações devem fazer com as orientações?

– ∀a, d, p, s Orientation(p, Result(a, s)) = d ⇔ [(a = T urn(Right) ∧ d = Mod(Orientation(p, s) − 90, 360)) ∨ (a = T urn(Left) ∧ d = Mod(Orientation(p, s) + 90, 360)) ∨ (Orientation(p, s) = d ∧ ¬(a = T urn(Right) ∨ a = T urn(Left)))]

– Além disso deve saber o q fazer quando está com o ouro e se o wumpus está vivo ou morto (descrição de Shoot).

[figure]

Lógica de Primeira Ordem

• Dedução de “propriedades escondidas”.

– ∀l, s At(Agent, l, s) ∧ Brisa(s) ⇒ F resco(l)

– ∀l, s At(Agent, l, s) ∧ MauCheiro(s) ⇒ MauCheiroso(l)

• Regras sincrônicas para relacionar propriedades de um estado ao mesmo estado.

– Causais (sistemas baseados em modelos):

∗ ∀l_{1}, l_{2}, s At(W umpus, l_{1}, s) ∧ Adj(l_{1}, l_{2}) ⇒ MauCheiroso(l_{2})

∗ ∀l_{1}, l_{2}, s At(Buraco, l_{1}, s) ∧ Adj(l_{1}, l_{2}) ⇒ F resco(l_{2})

– Diagnósticas (sistemas baseados em diagnósticos): ∗ ∀l, s At(Agent, l, s) ∧ Brisa(s) ⇒ F resco(l)

∗ ∀l, s At(Agent, l, s) ∧ MauCheiro(s) ⇒ MauCheiroso(l)

∗ ∀l_{1}, s MauCheiroso(l_{1}) ⇒ (∃l_{2} At(W umpus, l_{2}, s) ∧ (l_{2} = l_{1} ∨ Adj(l_{1}, l_{2}))

Lógica de Primeira Ordem

• ∀x, y, g, u, c, s P ercept([N, N, g, u, c], t) ∧ At(Agent, x, s) ∧ Adj(x, y) ⇒ OK(y) (regra fraca).

• ∀x, t(¬ At(W umpus, x, t) ∧ ¬ Buraco(x)) ⇔ OK(x) (regra mais forte).

• Conclusão: se os axiomas descrevem completamente e corretamente a forma como o mundo opera e a forma como as percepções são produzidas, então o procedimento de infereência vai inferir a melhor descrição possível de estados no mundo dadas as percepções.

[figure]

Lógica de Primeira Ordem

• Prioridades para as ações: dada uma determinada situação, podemos escolher entre várias ações.

• ∀a, sGreat(a, s) ⇒ Action(a, s)

• ∀a, sGood(a, s) ∧ (¬∃b Great(b, s)) ⇒ Action(a, s)

• ∀a, sMedium(a, s) ∧ (¬∃b Great(b, s) ∨ Good(b, s)) ⇒ Action(a, s)

• ∀a, sRisky(a, s) ∧ (¬∃b Great(b, s) ∨ Good(b, s) ∨ Medium(b, s)) ⇒ Action(a, s)

• sistemas que usam este tipo de regra: action-value.

[figure]

Lógica de Primeira Ordem

• Descrições anteriores não dizem nada sobre as ações. Apenas classificam as ações.

• ações do tipo Great consistem em pegar o ouro quando este for encontrado e pular para fora da caverna com o ouro.

• ações do tipo Good consistem em mover para uma posição que é OK, mas que não foi ainda visitada.

• ações do tipo Medium consistem em mover para uma posição que está OK, mas que já foi visitada.

• ações do tipo Risky consistem em mover para uma posição em que não se conhece a situação.

[figure]

Lógica de Primeira Ordem

• Agente baseado em Objetivos: tenta alcançar os objetivos.

• uma vez que o ouro foi encontrado, a política de movimentação na caverna muda radicalmente: devemos voltar à posição inicial o mais rápido possível.

• ∀s Holding(Ouro, s) ⇒ GoalLocation([1, 1], s)

• três formas de encontrar uma sequência de passos que levem a algum objetivo:

– Inferência

– Busca (pe, best-first search)

– Planning: sistemas de raciocínio orientados para ações.

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem

• Mesmas regras de cálculo de predicados proposicional podem ser aplicadas.

• Precisamos de mais regras para tratamento de variáveis.

• Substituição de variáveis por constantes individuais:

SUBST (θ, α).

• Ex:

SUBST ({x/Sam, y/P am}, Likes(x, y)) = Likes(Sam, P am)

• três novas regras: Elimin Universal Elimin Existencial \frac{∀vα}{SUBST (\{v/g\},α)} \frac{∃vα}{SUBST (\{v/k\},α)} Introd Existencial \frac{α}{∃vSUBST (\{g/v\},α)}

• Importante: eliminação existencial deve fazer substituições por constantes que ainda não tenham aparecido no KB!

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem

• Exemplo de prova: “A lei americana diz que é crime um americano vender armas para nações hostis. Nono, um país inimigo dos EUA, tem alguns mísseis, e todos estes mísseis foram vendidos pelo Coronel Oeste, que é americano”. Provar que o coronel é criminoso.

• ...é um crime um americano vender armas para nações hostis...

• (1) ∀x, y, zAmer(x) ∧ Arma(y) ∧ Nacao(z) ∧ Hostil(z) ∧ V ende(x, z, y) ⇒ Crim(x)

• ...Nono...tem alguns mísseis...

• (2) ∃xDono(Nono, x) ∧ Missil(x)

Cap. 9: Inferência em Lógica de Primeira Ordem • ...todos estes mísseis foram vendidos pelo Coronel Oeste...

• (3) ∀xDono(Nono, x) ∧ Missil(x) ⇒ V ende(Oeste, Nono, x)

• (4) ∀xMissil(x) ⇒ Arma(x)

• (5) ∀xInimigo(x, EUA) ⇒ Hostil(x)

• (6) Americano(Oeste), (7) Nacao(Nono), (8)

Inimigo(Nono, EUA), (9) Nacao(EUA)

Cap. 9: Inferência em Lógica de Primeira Ordem • (10) De (2) e elim exist: Dono(Nono, M1) ∧ Missil(M1)

• (11) e (12) De (10) e elim E: Dono(Nono, M1), Missil(M1)

• (13) De (4) e elim univ: Missil(M1) ⇒ Arma(M1)

• (14) De (12), (13) e Modus Ponens: Arma(M1)

• (15) De (3) e elim univ:

Dono(Nono, M1) ∧ Missil(M1) ⇒ V ende(Oeste, Nono, M1)

• (16) De (15), (10) e Modus Ponens: V ende(Oeste, Nono, M1)

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem • (17) De (1) e elim univ (3x):

Amer(Oeste) ∧ Arma(M1) ∧ Nacao(Nono) ∧ Hostil(Nono) ∧ V ende(Oeste, Nono, M1) ⇒ Crim(Oeste)

• (18) De (5) e elim univ:

Inimigo(Nono, EUA) ⇒ Hostil(Nono)

• (19) De (8) e (18) e Modus Ponens: Hostil(Nono)

• (20) De (6), (7), (14), (16), (19) e introd E: Amer(Oeste) ∧ Arma(M1) ∧ Nacao(Nono) ∧ Hostil(Nono) ∧ V ende(Oeste, Nono, M1)

• (21) De (17), (20) e Modus Ponens: Crim(Oeste)

Cap. 9: Inferência em Lógica de Primeira Ordem • Observações:

– Esta prova é a solução para um problema de busca, se formulássemos este problema como um problema de busca.

– O algoritmo deveria ser bastante esperto para não seguir

caminhos errados.

• Formulado como um problema de busca: – estado inicial: KB, sentenças de 1 a 9.

– operadores: regras de inferência.

– estado final: KB contendo Crim(Oeste).

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem

• 14 passos de prova.

• fator de ramificação aumenta de acordo com o aumento do KB.

• Elim univ pode ter um fator de ramificação muito grande, porque podemos substituir as variáveis por qualquer termo “ground”.

• Tempo gasto em conjunções, instanciação de variáveis e aplicação de Modus Ponens.

• problema com Modus Ponens é que somente faz deduções sobre termos “ground”.

• Métodos mais eficientes de prova.

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem

• Modus Ponens Generalizado.

• um único passo para intr E, elim univ e Modus Ponens.

• Idéia: inferir de KB = Missil(M1), Dono(Nono, M1), ∀xMissil(x) ∧ Dono(Nono, x) ⇒ V ende(Oeste, Nono, x), num único passo: V ende(Oeste, Nono, M1)

• se existir uma substituição θ tal que

SUBST (θ, pi^{′}) = SUBST (θ, p_{i})

• ^{\frac{p′_{1},p′_{2},...,p′_{n},(p_{1}∧p_{2}∧...∧p_{n}⇒q)}{SUBST (θ,q)}}
p1^{′} is Missil(M1)  p_{1} is Missil(x)
p2^{′} is Dono(y, M1)  p_{2} is Dono(Nono, x)
θ is {x/M1,y/Nono} q is V ende(Oeste, Nono, x)

SUBST (θ, q) is V ende(Oeste, Nono, M1)

Cap. 9: Inferência em Lógica de Primeira Ordem

• Modus Ponens Generalizado é uma regra de inferência eficiente por três razões:

– usa “passos largos”, combinando várias inferências pequenas em apenas uma.

– usa passos coerentes, usa substituições que são garantidamente úteis, invés de aplicar elim universal de forma aleatória.

– usa um passo de pre´-compilação para converter todas as sentenças do KB em forma canônica (forma da regra obriga a isto).

[figure]

Cap. 9: Inferência em Lógica de Primeira Ordem

• Forma canônica: todas as fórmulas no KB são fórmulas atômicas ou uma implicação com uma conjunção de fórmulas atômicas como antecedente e um único átomo/literal como consequente → sentenças de Horn.

• um KB contendo somente sentenças de Horn: Forma Normal de Horn.

• sentenças são transformadas em sentenças de Horn qdo dão entrada no KB. Ex: ∃xDono(Nono, x) ∧ Missil(x) é transformada em duas novas sentenças através de elim exist e elim E.

• uma vez que todos os quantif exist são eliminados, podemos dispor do quantif univ. Assume-se que todas as variáveis estão quantif universalmente.

• Nem toda sentença pode ser convertida em sentença de Horn.

Cap. 9: Inferência em Lógica de Primeira Ordem • Unificação: pega duas sentenças atômicas e retorna uma

substituição que faz as duas sentenças parecerem a mesma.

• UNIF Y (p, q) = θ, com SUBST (θ, p) = SUBST (θ, q).

• θ: unificador das duas sentenças.

• Ex: Conhece(Joao, x) ⇒ Odeia(Joao, x)

• KB: Conhece(Joao, Jane), Conhece(y, Leonardo), Conhece(y, Mae(y)), Conhece(x, Elisabete)

Cap. 9: Inferência em Lógica de Primeira Ordem • Aplicando Unificação:

• UNIF Y (Conhece(Joao, x), Conhece(Joao, Jane)) = {x/Jane}

• UNIF Y (Conhece(Joao, x), Conhece(y, Leonardo)) = {x/Leonardo, y/Joao}

• UNIF Y (Conhece(Joao, x), Conhece(y, Mae(y))) = {y/Joao, x/Mae(Joao)}

• UNIF Y (Conhece(Joao, x), Conhece(x, Elisabete)) = falha!