Visão Geral dos Provadores Automáticos de Teoremas

(em construção)

(...)

O que é Prova Automática de Teoremas?

Prova Automática de Teoremas (Automated Theorem Proving ou ATP) trata do desenvolvimento de programas de computador que mostram que cerca de afirmação (a conjectura) é uma consequência lógica de um conjunto de afirmações (os axiomas e hipóteses). Sistemas de ATP são utilizados em uma ampla variedade de domínios. Por exemplo, um matemático poderia provar a conjectura de que grupos de ordem dois são comutativos, a partir dos axiomas da teoria dos grupos; um consultor de gestão poderia formular axiomas que descrevem como as organizações crescem e interagem, e a partir destes axiomas provar que as taxas de óbito organizacional diminuem com a idade; um desenvolvedor de hardware poderia validar a concepção de um circuito provando uma conjectura que descreve o desempenho do circuito, dados axiomas que descrevem o circuito em si, ou um adolescente frustrado pode formular as faces misturadas de um cubo Rubik como uma conjectura e provar, a partir de axiomas que descrevem mudanças legais para a configuração do cubo, que o cubo pode ser reajustado para o estado de solução. Todas estas são tarefas que podem ser executadas por um sistema de ATP, dada uma adequada formulação do problema como axiomas, hipóteses, e uma conjectura.

(...)

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