Lógica de Primeira Ordem: Forward Chaining

• renomeia variáveis e compõe substituições.

• Composição de substituições:

SUBST (COMP OSE(θ_{1}, θ_{2}), p) = SUBST (θ_{2}, SUBST (θ_{1}, p))

Lógica de Primeira Ordem: Forward Chaining

procedure FORWARD-CHAIN(KB,p) if há uma sent em KB que renomeia p then return adiciona p a KB for each (p_{1} ∧ … ∧ p_{n}) → q em KB tal que para algum i, UNIF Y (p_{i}, p) = θ sucede do FIND-AND-INFER(KB,[p_{1}, …, p_{i−1}, p_{i+1}, …, p_{n}], q, θ)

end

Lógica de Primeira Ordem: Forward Chaining

procedure FIND-AND-INFER(KB,premises,conclusion,θ)

if premises = [] then

FORWARD-CHAIN(KB,SUBST(θ,conclusion)) else for each p′ em KB tal que UNIFY(p′,

SUBST(θ, FIRST(premises))) = θ_{2} do FIND-AND-INFER(KB,REST(premises),conclusion,

COMPOSE(θ,θ_{2})) end

Lógica de Primeira Ordem: Forward Chaining

• (1)

Amer(x) ∧ Arma(z) ∧ Nacao(y) ∧ Hostil(y) ∧ V ende(x, z, y) ⇒ Crim(x)

• (2) Dono(Nono, x) ∧ Missil(x) ⇒ V ende(Oeste, Nono, x)

• (3) Missil(x) ⇒ Arma(x)

• (4) Inimigo(x, EUA) ⇒ Hostil(x)

[figure]

Lógica de Primeira Ordem: Forward Chaining

• Inicialmente KB contém somente as implicações de Horn, adiciona-se cada fato de cada vez.

• FORWARD-CHAIN(KB,Amer(Oeste)): adiciona fato ao KB, unifica com uma premissa de (1), mas as outras não são conhecidas, então termina.

• FORWARD-CHAIN(KB,Nacao(Nono)): adiciona fato ao KB, unifica com uma premissa de (1), mas as outras não são conhecidas, então termina.

• FORWARD-CHAIN(KB,Inimigo(Nono,EUA)): adiciona fato ao KB, unifica com premissa de (3), com MGU {x/Nono}, chama:

– FORWARD-CHAIN(KB,Hostil(Nono)): adiciona fato ao KB, unifica com uma premissa de (1), mas somente duas são conhecidas, então termina.

Lógica de Primeira Ordem: Forward Chaining

• FORWARD-CHAIN(KB,Dono(Nono,M1)): adiciona fato ao KB, unifica com premissa de (2), com MGU {x/M1}, mas outra premissa ainda não conhecida, então termina.

• FORWARD-CHAIN(KB,Missil(M1)): adiciona fato ao KB, unifica com premissa de (2) e (3):

– Por (2) Missil(M1), MGU {x/M1}, como Dono(Nono,M1) já foi provado, chama:

∗ FORWARD-CHAIN(KB,Vende(Oeste,Nono,M1)): adiciona fato ao KB, unifica com uma premissa de (1), com MGU {x/Oeste,y/M1,z/Nono}, mas Arma(M1) não é conhecida, então termina.

Lógica de Primeira Ordem: Forward Chaining

• Por (3) Missil(M1), MGU {x/M1}, chama:

– FORWARD-CHAIN(KB,Arma(M1)): adiciona fato ao KB, unifica com uma premissa de (1), com MGU {y/M1}, outras premissas conhecidas com MGU acumulado {x/Oeste,y/M1,z/Nono}, chama:

∗ FORWARD-CHAIN(KB,Crim(Oeste)): adiciona fato ao KB, terminada a prova!

Lógica de Primeira Ordem: Backward Chaining

• Algoritmo Forward Chaining implementa um procedimento dirigido a dados. Pode ser incorporado ao procedimento TELL.

• Pode gerar conclusões irrelevantes.

• Algoritmo mais dirigido à consulta: Backward Chaining.

• Encontra todas as soluções para uma determinada pergunta ao KB.

• Pode ser incorporado ao procedimento ASK.

Lógica de Primeira Ordem: Backward Chaining

[figure]

Lógica de Primeira Ordem: Completude • Qq procedimento de prova usando Modus Ponens é incompleto.

• Mas se uma sentença for consequência lógica do KB, então existem algoritmos que são completos. Se a sentença não for consequência lógica do KB, então o procedimento pode entrar em loop (Teorema da Completude de Gödel): if KB ⊨ α then KB ⊢_{R} α.

• Problema da validade de lógica de primeira ordem é semi-decidível.

• Problema com Modus Ponens: sentenças com literais negados.

• ∀xP (x) ⇒ Q(x)

• ∀x¬P (x) ⇒ R(x)

• ∀xQ(x) ⇒ S(x)

• ∀xR(x) ⇒ S(x)

[figure]

Lógica de Primeira Ordem: Algoritmo de Resolução • Relembrando regra de resolução de lógica proposicional:

• \frac{α∨β,¬β∨γ}{α∨γ} ou \frac{¬α⇒β,β⇒γ}{¬α⇒γ}

• Duas interpretações: raciocínio por casos ou transitividade da implicação.

• Modus Ponens não permite derivar novas implicações. Somente deriva conclusões atômicas.

• Regra de resolução mais poderosa.

• Regra de resolução generalizada: procedimento de infereência completo para lógica de primeira ordem.

Lógica de Primeira Ordem: Algoritmo de Resolução

• Regra de Resolução generalizada (disjunções):

\frac{p_{1} ∨ … ∨ p_{j} ∨ … ∨ p_{m} q_{1} ∨ … ∨ q_{k} ∨ … ∨ q_{n}}{SUBST (θ, (p_{1} ∨ … p_{j−1} ∨ p_{j+1} … p_{m} ∨ q_{1}, ∨ … q_{k−1} ∨ q_{k+1} ∨ … q_{n}))}

• Regra de Resolução generalizada (implicações):

\frac{p_{1} ∧ … p_{j} ∧ … p_{n_{1}} ⇒ r_{1} ∨ … r_{n_{2}} s_{1} ∧ … s_{n_{3}} ⇒ q_{1} ∨ … q_{k} ∨ … q_{n_{4}}}{SUBST (θ, (p_{1} ∧ … p_{j−1} ∧ p_{j+1} ∧ p_{n_{1}} ∧ s_{1} ∧ … s_{n_{3}} ⇒ r_{1} ∨ … r_{n_{2}} ∨ q_{1} ∨ …))}

Lógica de Primeira Ordem: Algoritmo de Resolução • Formas canônicas para resolução: forma conjuntiva normal ou

forma implicativa normal.

\begin{matrix}¬P (w) ∨ Q(w) & P (w) ⇒ Q(w) \\ P (x) ∨ R(x) & T rue ⇒ P (x) ∨ R(x) \\ ¬Q(y) ∨ S(y) & Q(y) ⇒ S(y) \\ ¬R(z) ∨ S(z) & R(z) ⇒ S(z) \end{matrix}

• Resolução é uma generalização de Modus Ponens:

\frac{α, α ⇒ β}{β} ⇔ \frac{T rue ⇒ α, α ⇒ β}{T rue ⇒ β}

Lógica de Primeira Ordem: Algoritmo de Resolução • Provas por Resolução: forward chaining ou backward chaining.

Lógica de Primeira Ordem: Algoritmo de Resolução • Prova usando resolução ainda é não completa se não tivermos

nada no KB. Ex: p ∨ ¬p. é válida, mas resolução não pode resolver se KB estiver vazio.

• Procedimento de inferência completo usando resolução: refutação (redução ao absurdo ou prova por contradição).

• Para provar P, assume-se que P é falso adicionando-se ¬P ao KB. Em outras palavras: (KB ∧ ¬P ⇒ F also) ⇔ (KB ⇒ P).

• resolução usando refutação é completo e correto.

[figure]

Lógica de Primeira Ordem: Conversão para Forma Normal

• Qq sentença em lógica de primeira ordem pode ser convertida em forma implicativa (ou conjuntiva) normal.

• Passos para conversão:

1. Eliminação de implicações.

2. Mover negações para dentro dos parênteses.

3. Renomear variáveis (padronização separada).

4. Mover quantificadores para a esquerda.

5. “Skolemização”: ∀xP essoa(x) ⇒ ∃yCor(y) ∧ T em(x, y).

6. Distribuição de ∧ sobre ∨: (a ∧ b) ∨ c.

7. Agrupamento de conjunções e disjunções aninhadas: (a ∨ b) ∨ c.

8. Conversão de disjunções para forma implicativa: (¬a ∨ ¬b ∨ c ∨ d).

[figure]

Lógica de Primeira Ordem: Exemplo de Prova Joao tem um cachorro. Todo dono de cachorro ama animais. Ninguém que ama animais mata animais. Joao ou a Curiosidade matou o gato, cujo nome é Atum. A Curiosidade matou o gato?

A. ∃xCach(x) ∧ Dono(Joao, x) B. ∀x(∃yCach(y) ∧ Dono(x, y)) ⇒ AmaAnimais(x) C. ∀xAmaAnimais(x) ⇒ ∀yAnimal(y) ⇒ ¬Mata(x, y) D. Mata(Joao, Atum) ∨ Mata(Curiosidade, Atum) E. Gato(Atum) F. ∀xGato(x) ⇒ Animal(x)

Lógica de Primeira Ordem: Igualdade de Termos

• P(A) não unifica com P(B) mesmo que exista um fato no KB dizendo que A=B.

• Unificação faz somente testes sintáticos para verificar se dois termos são iguais.

• duas formas de resolver o problema: axiomatização da igualdade ou nova regra de inferência: demodulação/paramodulação.

Lógica de Primeira Ordem: Estratégias de Resolução • Principal preocupação: eficiência do método.

• Preferência por sentenças unitárias (atômicas).

• Conjunto de Suporte.

• Resolução de Entrada, Resolução Linear.

• Subsumption: elimina sentenças que são mais específicas do que qq sentença existente no KB.