|
|
| Linha 1: |
Linha 1: |
| − |
| |
| − |
| |
| | == Lista não organizada == | | == Lista não organizada == |
| | | | |
| | * Verit. Site: http://www.verit-solver.org/ | | * 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.
| |
| | | | |
| | == Links == | | == Links == |
