[figure]

Lógica de Primeira Ordem

• Solução: renomear variáveis (padronização separada de duas sentenças).

• UNIF Y (Conhece(Joao, x_{1}), Conhece(x_{2}, Elisabete)) = {x_{1}/Elisabete, x_{2}/Joao}

• UNIFY deveria retornar substituições que façam os dois argumentos parecerem os mesmos. Há uma qtde infinita de substuições deste tipo: unificador mais geral (MGU).

• Ex: UNIF Y (Conhece(Joao, x), Conhece(y, z))

– {y/Joao, x/z} unif. + geral

– {y/Joao, x/z, w/F rida}

– {y/Joao, x/Joao, z/Joao} etc.

[figure]

Lógica de Primeira Ordem

• Voltando à prova de que Coronel Oeste é criminoso...

• Sentenças (1) a (9) ficam:

– (22)

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

– (23) Dono(Nono, M1)

– (24) Missil(M1)

– (25) Dono(Nono, x) ∧ Missil(x) ⇒ V ende(Oeste, Nono, x)

– (26) Missil(x) ⇒ Arma(x)

– (27) Inimigo(x, EUA) ⇒ Hostil(x)

– (28) Amer(Oeste, (29) Nacao(Nono), (30)

Inimigo(Nono, EUA), (31) Nacao(EUA)

Lógica de Primeira Ordem

• Prova: 4 passos.

– (32) De (24) e (26), usando Modus Ponens: Arma(M1)

– (33) De (30) e (27), usando Modus Ponens: Hostil(Nono)

– (34) De (23), (24) e (25), usando Modus Ponens:

V ende(Oeste, Nono, M1)

– (35) De (28), (32), (29), (33), (34) e (22): Crim(Oeste)

• Algoritmos que usam Modus Ponens formam a base para várias aplicações de grande escala em IA.

Lógica de Primeira Ordem

• Forward Chaining x Backward Chaining.

• Forward Chaining: partimos de sentenças do KB e tentamos deduzir novas sentenças que sejam conseqüências lógicas do KB. Usado normalmente qdo um novo fato é adicionado ao KB.

• Backward Chaining: partimos de uma sentença que desejamos provar que é verdadeira.