Galculator

O Galculator é um protótipo de um assistente de prova baseado na álgebra das conexões de Galois. Quando combinadas com a transformada pointfree e tácticas com a igualdade indirecta, as conexões de Galois oferecem um dispositivo poderoso e genérico para abordar a complexidade das provas.

O protótipo do Galculator está a ser desenvolvido no âmbito de um projecto de doutoramento em curso. Está escrito na linguagem de programação Haskell, e utiliza várias extensões da linguagem, sobretudo GADTs (Generalized Algebraic Data Types).

Download

Apesar de ser ainda experimental e mudar rapidamente, o código pode ser obtido a partir do repositório SVN.

Documentação

Ainda não existe documentação da ferramenta. Esperamos resolver isso em breve.

Novos desenvolvimentos

Actualmente, estamos a trabalhar na derivação automática dos chamados "teoremas-grátis" das funções polimórficas e a sua aplicação às provas. Também estão a ser estudadas construções mais complexas de conexões de Galois. Finalmente, temos planos para a integração do Galculator com um provador de teoremas, nomeadamente o Coq.

Contacto

Para qualquer informação, contacte Paulo Silva
email
homepage