Demonstração por árvore de refutação

                                               Árvore de refutação, execício resolvido

 Dada uma lista de Wffs, uma árvore de refutação é uma busca exaustiva de caminhos nos quais toda Wffs da lista pode ser verdadeiras. A busca é executada desmembrando as Wffs da lista em letras sentenciais ou suas negações. Se encontrarmos alguma atribuição de verdade e falsidade para as letras sentenciais que torne verdadeiras todas as Wffs da lista, então, sob essa atribuição, as premissas da forma são verdadeiras enquanto enquanto sua conclusão é falsa. Assim, refuta-se a forma de argumento; ela é inválida. Se na busca não surgir atribuição de verdade e falsidade para as letras sentenciais que torne verdadeiras toda Wffs da lista, então a refutação falha; a forma é válida.