Lógicas Clássicas
Prova Automática de Teoremas
- 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.