•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.