Visão Geral dos Provadores Automáticos de Teoremas

(em construção)

(...)

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

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

Many significant problems have been, and continue to be, solved using ATP. The fields where the most notable successes have been achieved are mathematics, software creation and verification, and hardware verification, and knowledge based systems.

The most exciting recent success in mathematics has been the settling of the Robbins problem by the ATP system EQP. In 1933 Herbert Robbins conjectured that a particular group of axioms form a basis for Boolean algebra, but neither he nor anyone else (until the solution by EQP) could prove this. The proof that confirms that Robbins' axioms are a basis for Boolean algebra was found October 10, 1996, after about 8 days of search by EQP, on an RS/6000 processor. This result was reported in the New York Times.

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