Resumo

Este trabalho se propõe a apresentar o provador 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, o provador utiliza de uma fórmula estruturada em XML que passa por um interpretador que ler e a transforma numa estrutura computacional construída para tornar possível a utilização do método de “árvore de refutação”. A validação resulta numa representação gráfica da “árvore de refutação”. Tais processos de validação e visualização da árvore foram separados em back-end e front-end, que se comunicam para realizar a validação automática de fórmulas do cálculo proposicional.