Visão Geral dos Provadores Automáticos de Teoremas

(em construção)

(...)

Siglas

ATP = Automated Theorem Proving (Prova Automática de Teoremas)

Para que a Prova Automática de Teoremas tem sido realmente útil?

Muitos problemas significativos foram, e continuam a ser resolvidos por meio ATP. Os campos onde os sucessos mais notáveis foram atingidos são matemática, criação e verificação de software, e verificação de hardware, e sistemas baseados em conhecimento.

O mais recente e emocionante sucesso em matemática foi a resolução do problema de Robbins pelo sistema de ATP "EQP". Em 1933 Herbert Robbins conjecturou que um grupo particular de axiomas formam uma base para uma ágebra booleana, mas nem ele nem qualquer outra pessoa (até que a solução foi obtida pelo sistema EQP) conseguiu provar isso. A prova que confirma que os axiomas de Robbins são uma base para uma álgebra booleana foi encontrada em 10 de outubro de 1996, após cerca de 8 dias de busca pelo EQP, em um processador RS/6000. Este resultado foi relatado no New York Times.

(...)

Tradução e Adaptação do texto de Geoff Sutcliffe, disponível em http://www.cs.miami.edu/~tptp/OverviewOfATP.html