Introdução e Histórico

• Histórico

  • Gödel e Herbrand na década de 30 mostraram que que qualquer fórmula verdadeira pode ser provada.
  • Church e Turing em 1936 mostraram que não existe um método geral capaz de decidir, em um número finito de passos, se uma fórmula é verdadeira.
  • Um dos primeiros objetivos da IA foi a Prova Automática de Teoremas, a partir da segunda metade da década de 60, sendo que a partir daí a lógica passou a ser estudada com método computacional para a solução de problemas.
  • O método explora o fato de expressões lógicas poderem ser colocadas em formas canônicas (apenas com operadores “e”, “ou” e “não”). O resultado permite a manipulação computacional bastante eficiente.

Slide anterior

Slide seguinte

Voltar para o primeiro slide

Exibir versão do elemento gráfico