Prezados, 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. Atenciosamente, -- David Deharbe. _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
