Bruno Vilar Vilar, B.

Parcilene Fernandes de Brito Brito, P. F.

Resumo

Provadores automáticos de teoremas são programas que utilizam regras de inferência para a verificação da validade ou invalidade de fórmulas lógicas. Ao realizar a apresentação dos passos necessários à prova, tem-se a possibilidade de auxiliar no estudo da Lógica Quantificacional. O presente trabalho tem por objetivo o desenvolvimento de uma das etapas da construção de um Editor, que antecede a apresentação das etapas de prova, a validação dos dados de entrada e criação de um documento XML, realizados por um parsing.