Lógica para Computação - Método da Resolução: Cláusulas de Horn - aula10

Prévia do material em texto

IF673 – Engenharia da Computação 
Cin/UFPE – Anjolina Grisi de Oliveira 
2 
Método da Resolução 
 {CD, (BD), A(BC)} | A 
 
 { (LM)P, IP, M, I } | L 
Cláusula de Horn: possui no máximo um literal 
positivo 
Ao usar apenas cláusulas de Horn, o método da 
resolução tem um custo computacional baixo, ou 
seja, linear em função do tamanho da fórmula. 
 { (AB), (AC), (DB)} | (CD) 
3 
Considerações sobre o Tableaux 
 Vantagens 
• Mais eficiente que a tabela-verdade em 
alguns casos (quais?) 
• Mais intuitivo 
 Desvantagem principal 
• Não há uma maneira de se determinar em 
que casos o método é eficiente 
4 
Cláusulas de Horn 
 Em meados da década de 1950, o lógico Alfred Horn 
trabalhou na chamada ``lógica de sentenças condicionais´´, 
isto é, na lógica que envolve sentenças do tipo: 
 
 se fato 1 
 fato 2 
 e 
 ..... 
 fato n 
 então 
 conclusão 
(f1f2f3f4c)  (f1f2f3f4 )c f1f 2f3f4c