Provadores de Teoremas
Lista não organizada
- Verit. Site: http://www.verit-solver.org/
Na oportunidade da conferência CADE-22, ocorrendo atualmente em Montreal, Canadá, foi lançada o veriT-200907, um provador automático de teoremas na família dos "SMT-solvers" (resolvedores de satisfatibilidade módulo teoria?), desenvolvido em uma colaboração entre a UFRN, o LORIA e a Universidade de Nancy 2.
veriT tem como linguagem de entrada o formato SMT-LIB (www.smtlib.org) estendido com lambda expressões e macro definições. Ainda é gerador de prova, é publicado com uma licença aberta, e é razoavelmente eficiente.
Nesta versão, e usando a nomenclatura SMT-LIB, veriT trata de forma completa as lógicas de primeira ordem sem quantificadores chamadas 1- QF_UF (com predicados e funções não interpretados), 2- QF_IDL (lógica de diferença sobre os inteiros), 3- QF_RDL (lógica de diferença sobre os números reais), e 4- QF_UFIDL (combina QF_UF e QF_IDL).
Interessados são convidados a visitar o sítio do veriT, hospedado no endereço "http://www.verit-solver.org" onde poderão obter o código fonte da ferramenta, junto com instruções de compilação e instalação.
No momento, veriT está sendo melhorado para ser mais eficiente, tratar de forma completa restrições de aritmética linear sobre números reais e números inteiros, e aprimorar as heurísticas de instanciação de quantificadores.
