Lógicas Clássicas
Prova Automática de Teoremas
- A capacidade de se demostrar teoremas é uma das partes integrantes da inteligência humana.
- Este tipo de prova foi pesquisada e desenvolvida a partir da segunda metade dos anos 60.
- A partir da introdução, por Robinson e Smullyan, em 1960,de procedimentos eficientes para demonstração automática de teoremas por computador, a lógica passou a ser estudada também como método computacional para a solução de problemas.
- Uma das áreas que mais faz uso desta técnica é a dos Sistemas Especialistas (SEs).
- O objetivo principal da Prova Automática de Teoremas é provar que uma fórmula (teorema) é conseqüência lógica de outras fórmulas.