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.
–Os métodos adotados normalmente não utilizam a prova direta (através de regras de inferência), mas sim a PROVA POR REFUTAÇÃO (prova indireta), demonstrando que a negação da fórmula leva a inconsistências.
–SE A NEGAÇÃO DE UM TEOREMA É FALSA, ENTÃO ELE SERÁ VERDADEIRO.
–Os procedimentos de prova exploram o fato de expressões lógicas (fórmulas) poderem ser colocados em formas canônicas, isto é, apenas com os operadores “e”, “ou” e “não”.
–O método da prova por refutação aplicado à lógica de primeira ordem é muito conveniente e com seu emprego não haverá perda de generalidade, porém, exige-se que as fórmulas estejam na forma de cláusulas.