Prova por resolução

Abstract

Esta animação demonstra um conceito muito importante da lógica proposicional chamada prova por resolução. Tendo como principal ponto forte a simplicidade e utilizando apenas uma regra de inferência. Este tipo de resolução deve ser aplicado sempre às duas cláusulas para chegar a uma nova cláusula obtida pela eliminação dos átomos existentes nas cláusulas originais. Para se obter um resultado satisfatório, é necessário seguir três passos, são eles: a conversão de cada premissa para a Forma Normal Conjuntiva (FNC) e negar a conclusão, separar as cláusulas resultantes e por fim, construir a árvore de derivação ou de refutação a partir da aplicação de sucessivas aplicações da operação de resolução. Após a aplicação destas técnicas e não se chegar a uma cláusula vazia, ou seja, Nil indicando a validade de um argumento, este argumento será inválido.