Seminário de Lógica Aplicada a Computação

Árvore de Refutação e
Teorema de Herbrand

 Árvore de Refutação
 Cálculo Proposicional
 Método
 Regras de Construção
 Exemplos

 Cálculo de Predicados de 1ª Ordem
 Método
 Regras de Construção
 Exemplos

 Teorema de Herbrand

Árvore de Refutação – Cálculo Proposicional
Método:
 Método para verificar a validade de um argumento, onde
A1, A2, A3, ..., An são premissas do argumento e B é a conclusão deste.
Construção:
 Raiz – Uma lista de fórmulas consistindo das premissas do argumento e da negação da conclusão.
 Ramos – A partir de aplicações de regras (que serão especificadas posteriormente).

Árvore de Refutação – Cálculo Proposicional
Método:
Construção:
Conclusão – A árvore termina quando encontramos em seus ramos fórmulas que são:

 Variáveis Proposicionais
 Negação de Variáveis Proposicionais
Nesses casos, refutamos o argumento, isto é, o argumento não é válido.

 Ou em todos os ramos uma fórmula F

Nesse caso, a tentativa de refutação falhou ou seja, o argumento é válido.

Árvore de Refutação – Cálculo Proposicional
Regras de Construção:
Observações Iniciais:
 A fórmula será marcada ( ¬ ) para evitar aplicações repetidas de uma regra em uma mesma fórmula.
 A aplicação de uma regra deve gerar:
 uma ou duas linhas
 um ramo ou dois ramos conforme a regra, e será aplicada em todos os ramos abertos (não fechados com X) aos quais a fórmula pertence.