Bruno Vilar Vilar, B.

Parcilene Fernandes de Brito Brito, P. F.

Resumo

O presente trabalho tem por objetivo descrever o desenvolvimento do L-EditXML, um ambiente interativo que apresenta o processo de verificação da validade de fórmulas da Lógica Quantificacional e as etapas utilizadas para a sua prova. O ambiente está agregado a um provador de teoremas, que utiliza o método dos Tableaux e um algoritmo de unificação na construção das etapas de prova. Dessa forma, a partir da interação com o ambiente, o aluno-usuário poderá verificar a validade de fórmulas lógicas e, especialmente, compreender como a prova foi realizada.