Resumo Lógica - (FNC, Tableaux e Método de resolução)

Prévia do material em texto

TRANSFORMAÇÃO​ ​PARA​ ​FNC 
 
1. Eliminar​ ​os​ ​conectivos​ ​que​ ​nao​ ​pertencem​ ​ao​ ​fn​ ​(​ ​->​ ​​ ​​ ​<->​ ​);  
2. Eliminar a negação de cláusulas (somente pode haver negação de                   
símbolos​ ​proposicionais) 
3. Arrumar a disposição dos conectivos E( ^ ) e OU ( v ) para fora e                               
para​ ​dentro​ ​das​ ​cláusulas,​ ​respectivamente. 
 
 
MÉTODO​ ​DA​ ​RESOLUÇÃO 
 
1. Negar​ ​a​ ​tautologia​ ​a​ ​ser​ ​demonstrada; 
2. Substituir os conectivos <-> e -> utilizando as equivalências                 
clássicas​ ​(IMAGEM​ ​1); 
3. Levar​ ​a​ ​negação​ ​para​ ​dentro​ ​das​ ​cláusulas; 
4. Transformar​ ​a​ ​fórmula​ ​em​ ​FNC;  
5. Colocá-la​ ​na​ ​FCC​ ​(conjunto​ ​de​ ​cláusulas); 
6. Aplicar​ ​a​ ​regra​ ​de​ ​inferência​ ​(resolvente); 
● ​ ​​ ​Cláusula​ ​vazia​ ​->​ ​H​ ​é​ ​tautologia 
● ​ ​​ ​Saturação​ ​->​ ​H​ ​não​ ​é​ ​tautologia,​ ​H​ ​é​ ​satisfatível. 
 
 
TABLEAUX​ ​SEMÂNTICO 
 
1. Negar​ ​a​ ​tautologia​ ​a​ ​ser​ ​demonstrada; 
2. Aplicar​ ​as​ ​regras​ ​(IMAGEM​ ​2); 
● Fechado(todos​ ​os​ ​ramos​ ​fechados)​ ​->​ ​H​ ​é​ ​tautologia. 
● Aberto(algum ramo saturado e aberto) -> H não é tautologia, H é                       
satisfatível. 
​ ​  
​ ​​ ​​ ​​ ​​ ​​ ​Imagem​ ​1​ ​(acima) 
 
   
​ ​​ ​​ ​​ ​​ ​​ ​Imagem​ ​2