Lógicas das Proposições
Árvores de Refutação
2.10. Bicondicional Negado (? ?): Se um ramo aberto contém uma fórmula não ticada da forma ? (Ø ? ß), tica-se, ? (Ø ? ß) e BIFURCA-SE o final de cada ramo aberto que contém ? (Ø ? ß) ticada, no final do primeiro ramo se esreve Ø e ?ß e no final do segundo ramo se escreve ? Ø e ß.
As Tabelas-Verdade garantem a decidibilidade da lógica proposicional, porém elas são enfadonhas e ineficazes(NP-COMPLETAS) para um número muito grande de fórmulas-atômicas. Já as árvores de refutação fornecem um algoritmo mais eficaz para executar as mesmas tarefas.