| |
| Acadêmico(a): André Ramaciotti da Silva |
| Título: Provador interativo de teoremas com tipos dependentes |
| |
| Resumo: |
| Esta monografia de trabalho de conclusão de curso apresenta a especificação e a implementação de um provador interativo de teoremas baseado em uma linguagem formal com tipos dependentes. Com isso, mostra-se uma forma em que computadores podem auxiliar no desenvolvimento matemático e se introduz a teoria dos tipos dependentes a programadores em uma linguagem simplificada. De forma mais detalhada, objetiva-se especificar uma linguagem para descrever programas e teoremas de lógica de primeira ordem e um sistema de tipos baseado na teoria de tipos dependentes, implementar um interpretador de linha de comando e validar os programas e os teoremas de lógica de primeira ordem escritos nessa linguagem. Para isso, durante o desenvolvimento, é elaborada uma definição formal para a linguagem especificada através da notação Backus-Naur Form (BNF) e implementado um interpretador de linha de comando com a linguagem Haskell e a biblioteca Parsec. Ao final, todos os objetivos são alcançados, embora o uso da teoria de tipos dependentes faça com que a definição de certos tipos e funções se tornem mais complexa, além de restringir os teoremas que podem ser provados àqueles com provas construtivas. Faz-se também uma comparação com as linguagens Agda, Coq e a desenvolvida por Löh, McBride e Swierstra (2010), mostrando que a abordagem de Coq de separar as provas das definições de funções torna o código mais legível. |
| |
|
