Provadores Baseados em Unificação com Sorts

Arquivo em formato pdf. Texto contendo algoritmo utilizado no pré-processamento de reticulados para cálculo eficiente do maior descendente comum, algoritmo de unificação com sorts e proposta de uma linguagem de primeira ordem geral, declarativa e com semântica não determinada. Possui propostas de melhoramentos futuros e resultados de alguns testes. [download]

Árvores de prova

Arquivo em formato pdf. Relatório técnico contendo a descrição das implementações, o funcionamento do provador e resultados práticos obtidos com os testes realizados. [download]