An automated prover by tableaux for calculi C1 and C1* of Newton da Costa, by Arthur Buchsbaum

From Master's Thesis "Um Método Automático de Prova para a Lógica Paraconsistente", presented in 1988.


Download (5 Kbytes)

Code recovered in 2009, from a djvu scanning, thanks to Professor Adolfo Neto and his students. The original work was attacked by virus.

Fonte: http://wwwexe.inf.ufsc.br/~arthur/index.php?page=software&lang=en

Por onde começar?

Para começar a estudar provadores de teoremas, minha sugestão é que se leia o livro

SILVA, Flávio S. C. da; FINGER, Marcelo; MELO, Ana C. V. de. Lógica para Computação. São Paulo: Thomson Learning, 2006.

Este livro conquistou o primeiro lugar do Prêmio Jabuti 2007 na categoria Ciência Exatas, Tecnologia e Informática.

Sou um pouco suspeito para falar porque meu orientador de doutorado (Marcelo Finger) é um dos autores. Outro autor (Flávio Silva) estava na minha banca de qualificação de doutorado.

O livro contém alguns problemas de digitação (e talvez outros que eu ainda não tenha percebido). Merece sem dúvida ser lançada uma versão revisada.

Early History and Perspectives of Automated Deduction, Wolfgang Bibel

Neste blog colocarei links (liames) para textos, artigos e páginas de provadores de teoremas, entre outros recursos relacionados aos provadores. Começo com o texto abaixo, de Wolfgang Bibel.


Early History and Perspectives of Automated Deduction (em PDF)
Wolfgang Bibel

Abstract. With this talk we want to pay tribute to the late Professor Gerd Veenker who deserves the historic credit of initiating the formation of the German AI community. We present a summary of his scientific contributions in the context of the early approaches to theorem proving and, against this background, we point out future perspectives of Automated Deduction.

Formal logic is still often looked upon as a kind of esoteric doctrine.
Evert W. Beth 1958

The fundamental scientific progress lies in the area of logic and the cognitive sciences.
Pierre Papon 2006