Provadores de Teoremas
(→Links) |
|||
| Linha 1: | Linha 1: | ||
| + | |||
| + | |||
| + | == 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. | ||
| + | |||
== Links == | == Links == | ||
[http://www.cs.miami.edu/~tptp/OverviewOfATP.html Geoff Sutcliffe's Overview of Automated Theorem Proving] | [http://www.cs.miami.edu/~tptp/OverviewOfATP.html Geoff Sutcliffe's Overview of Automated Theorem Proving] | ||
[http://portal.acm.org/citation.cfm?id=645903.672930&coll=GUIDE&dl=GUIDE Effective Theorem Proving for Hardware Verification] | [http://portal.acm.org/citation.cfm?id=645903.672930&coll=GUIDE&dl=GUIDE Effective Theorem Proving for Hardware Verification] | ||
Edição de 19h20min de 6 de agosto de 2009
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.
