Danilo Saraiva Vicente Vicente, D. S.

Parcilene Fernandes de Brito Brito, P. F.

Resumo

Este trabalho se propõe a apresentar o módulo desenvolvido para realizar a verificação da validade de fórmulas da lógica proposicional por meio do método denominado “árvore de refutação”. Esse método verifica se uma dada fórmula é válida ou inválida pela tentativa de redução ao absurdo, ou seja, verifica se a negação da conclusão resulta em uma contradição. Para tanto, a ferramenta permite a verificação da validade de fórmulas de maneira automática e conforme a interação do usuário.