Procedimentos de Inferência

Forma Clausal

Literal: Fórmula atômica (negada ou não). [Sem quantificadores ou operadores]
Exemplos: S(x), P(x,y), Homem(Socrates), ~Homem(Joana),~P(x,y),...
~Exemplos: S(x)VP(x) , Vx(P(x)->Q(x)), ...

Cláusula: Fórmula que consiste unicamente da disjunção de literais.
Exemplos: P(x)VQ(y) , Homem(Socrates)v~Homem(Socrates) , P(x) v ~Q(x) v Z(x,Pedro)

Base de conhecimentos na Forma Clausal :  Conjunção de cláusulas
Exemplo: P(x) ^ Q(y)vR(w) ^ S(z)
Notação utilizando conjuntos: {P(x)},{Q(y),R(w)},{S(z)}

Converção para Forma Clausal

1. Eliminar Quantificadores Desnecessários.
Ex.: Vx ( Vy P(x,A) -> Q(x) ) , torna-se , Vx (P(x,A) -> Q(x) )
2. Renomear variáveis quantificadas mais de uma vez.
Ex.: Vx (P(x) -> Ex(Q(x) ) , torna-se, Vx (P(x) -> Ey (Q(y) )
3. Remover condicionais e bicondicionais usando fórmulas equivalentes.
Ex.: P(x) -> Q(x) , torna-se, ~P(x) v Q(x)
4. Remover negações externas usando as equivalências de DeMorgan e da Dupla Negação, além das seguintes:
~Vx(F) <=> Ex(~F) , onde F é uma fórmula qualquer.
~Ex(F) <=> Vx(~F)

Ex.: ~Vx( ~(P(x)vQ(x) ), torna-se, Ex( P(x) v Q(x) )

5. Eliminar quantificadores existenciais utilizando funções e constantes de Skolem (Skolemização)

Na Skolemização usamos constantes e funções para representar os objetos que o quantificador existencial 'garante como existentes'.

Quando o quantificador existencial se encontra dentro do escopo de um ou mais quantificadores universais, assumimos que essas constantes dependem das variáveis universalmente quantificadas.

Ex.: Vx (Ey (P(x,y) ), torna-se, Vx (P(x,F(x) ).
Ex.: Vx (Ey (Q(y)) , torna-se, Vx (Q(F(x))

Caso o quantificador existencial não esteja no escopo de um quantificador universal criamos uma nova constante (diferente de todas as outras) e a substituimos pelo predicado contendo a variável quantificada.

Ex.: Ey (P(y)) , torna-se, P(A)

6. Eliminar quantificadores universais

Ex.: Vx( P(x) ^ Vy( Q(x,y) )), torna-se, P(x) ^ Q(x,y)

7. Colocar a fórmula na forma conjuntiva  utilizando distributividade

Ex.: (P(x) ^ Q(x)) v R(x) , torna-se, (P(x) v R(x)) ^ (Q(x) v R(x))

8. Eliminar conjunções criando novas cláusulas
Ex.: (P(x) v R(x)) ^ (Q(x) v R(x)) , torna-se, {P(x) v R(x)} , {Q(x) v R(x)}
9. Aplicar notação de conjuntos
Ex.:  {P(x) v R(x)} , {Q(x) v R(x)}, torna-se, {P(x),R(x)} , {Q(x),R(x)}

Exemplo 1: Vx P(x) -> Ex (Q(x))  /* Obs: condicional tem prioridade sobre quantificador */
 
Passo Resultado
2 Vx P(x) -> Ey Q(y)
3 ~Vx P(x) v Ey Q(y)
4 Ex ~P(x) v Ey Q(y)
5 ~P(A) v Q(B)
8 {~P(A) v Q(B)}
9
 {~P(A),Q(B)}

Exemplo 2: VxVy (Ez (P(x,z) ^ P(y,z)) -> Eu Q(x,y,u))
 
Passo Resultado
3 VxVy(~Ez(P(x,z)^P(y,z)) v Eu Q(x,y,u))
4 VxVy( Vz(~(P(x,z)^P(y,z))) v Eu Q(x,y,u))
4 VxVy( Vz (~P(x,z) v ~P(y,z)) v Eu Q(x,y,u))
5 VxVy( Vz (~P(x,z) v ~P(y,z)) v Q(x,y,F(x,y)))
6 ~P(x,z) v ~P(y,z) v Q(x,y,F(x,y))
8 {~P(x,z) v ~P(y,z) v Q(x,y,F(x,y))}
9
 {~P(x,z),~P(y,z),Q(x,y,F(x,y))}

Exemplo 3: Vx (H(x) -> Ey (P(y) ^ C(x,y)))
 
Passo Resultado
3 Vx (~H(x) v Ey (P(y) ^ C(x,y)))
5 Vx (~H(x) v (P(F(x)) ^ C(x,F(x))))
6 ~H(x) v (P(F(x)) ^ C(x,F(x)))
7 (~H(x) v P(F(x))) ^ (~H(x) v C(x,F(x)))
8 {~H(x) v P(F(x))} ,{ ~H(x) v C(x,F(x))}
9
 {~H(x),P(F(x))} ,{ ~H(x),C(x,F(x))}

Estratégias de Resolução               

Cláusulas com literais complementares:  {P1, P2, ..., R, ..., Pn-1, Pn} e   {Q1, Q2, ..., ~R, ..., Qm-1, Qm}
Resolvente: {P1, P2, ..., Pn-1, Pn, Q1, Q2, ..., Qm-1, Qm} 
Teorema: s'
Premissas: t , t -> q'  ,  q' -> s'
Demonstração:

1
 {t}
 P
2
 {t',q'}
 P
3
 {q,s'}
 P
4
 {s}
PP
5
 {q'}
 R 1,2
6
 {t',s'}
 R 2,3
7
 {q}
 R 3,4
8
 {s'}
 R 1,6
9
 {t'}
 R 2,7
10
 {s'}
 R 3,5
11
 {t'}
 R 4,6
11
 {}
 R 4,8

* Exercício: demonstrar os teoremas em lógica proposicional, da seção técnicas de prova , utilizando a estratégia da resolução.

Exemplos em Cálculo de Predicados

1) Premissas:
1. P(H,B)    // Hilário é pai de Beatriz
2. P(H,J)     // Hilário é pai de Júlia
3. F(H,C)    // Hilário é filho de Carlos
4. Vx P(x,y) ^ P(y,z) -> A(x,z)
5. Vx P(x,y)<-> F(y,x)

Teorema: A(C,J)    [Carlos é avô de Júlia]

Cláusulas incluíndo negação do teorema: {P(H,B)}, {P(H,J)}, {F(H,C)}, {~P(x1,y1), ~P(y1,z1), A(x1,z1)}, {~P(x2,y2), F(y2,x2)}, {~F(y3,x3), P(x3,y3)}, {~A(C,J)}

Demonstração (resolução com conjunto de suporte):

{~A(C,J)}     {~P(x1,y1), ~P(y1,z1), A(x1,z1)}

        {x1/C,z1/J}
        {~P(C,y1),~P(y1,J)}           {P(H,J)}
                   {y1/H} 
                         {~P(C,H)}        {~F(y3,x3), P(x3,y3)}
                                {x3/C, y3/H}
                                      {~F(H,C)}          {F(H,C)}
                                          
                                                     {}

2) Teorema: A(C,x)    [Carlos é avô de quem ?]

Cláusulas incluíndo negação do teorema: {P(H,B)}, {P(H,J)}, {F(H,C)}, {~P(x1,y1), ~P(y1,z1), A(x1,z1)}, {~P(x2,y2), F(y2,x2)}, {~F(y3,x3), P(x3,y3)}, {~A(C,x4)}

Demonstração (resolução com conjunto de suporte):

{~A(C,x4)}     {~P(x1,y1), ~P(y1,z1), A(x1,z1)}
        {x1/C,z1/x4}
        {~P(C,y1),~P(y1,J)}           {P(H,J)} * ponto de backtracking
                   {y1/H} 
                         {~P(C,H)}        {~F(y3,x3), P(x3,y3)}
                                {x3/C, y3/H}
                                      {~F(H,C)}          {F(H,C)}
                                               
                                                     {}                           
                                                   

3) Linguagem natural: Aonde Carlos vai, Amélia também vai. Carlos está na praia. Amélia está na praia?

Cláusulas incluíndo negação do teorema: {~Estar(C,x1),EstaR(A,x1)} , {Estar(C,P)}, ~Estar(A,P)}

Demonstração (resolução com conjunto de suporte):

{~Estar(A,P)}            {~Estar(C,x1),Estar(A,x1)}
            {x1/P}
                        {~Estar(C,P)}               {Estar(C,P)}
                                 
                                                  {}

                  

4) Linguagem natural: (Problema dos candidatos - Conceitos Básicos)

Cláusulas incluíndo negação do teorema: {C(Lu)}, {C(Pa)}, {C(Ma)}, {~C(x1),L(x1),O(x1)}, {~L(x2),~G(x2,De)} , {~O(x3), G(x3,Co)},  {~G(Lu,x4),~G(Pa,x4)}, {G(Lu,x5),G(Pa,x5)}, {G(Lu,Co)}, {G(Lu,De)}, {~C(x6),~L(x6),O(x6)}

Demonstração (resolução com conjunto de suporte):

{~C(x6),~L(x6),O(x6)}       {~C(x1),L(x1),O(x1)}     * Backtracking
                      {x6/x1}
                      {~C(x1),O(x1)}                {C(Pa)}   * Backtracking
                                  {x1/Pa}
                                                {O(Pa)}            {~O(x3),G(x3,Co)} 
                                                       {x3/Pa}
                                                                 {G(Pa,Co)}        {~G(Lu,x4),~G(Pa,x4)}
                                                                          {x4/Co}
                                                                                   {~G(Lu,Co)}             {G(Lu,Co)}
                                                                                            
                                                                                                              {}

Considerações sobre Eficiência

Demonstração de teoremas utilizando resolução, na sua forma mais geral, é um problema NP-Completo.

Procedimentos eficientes podem ser obtidos aplicando-se restrições no formato das cláusulas

Cláusulas de Horn: Um ou nenhum literal positivo

Cláusulas Definidas: Exatamente um literal positivo (Prolog)