Negação por falha

Negação por falha é uma interpretação da negação lógica de acordo com a qual a negação de uma fórmula é verdadeira se e somente se a fórmula não pode ser provada verdadeira. A negação por falha é usada em linguagens de programação lógica como Prolog. Dessa forma em Prolog o compilador equipara a ausência de evidência com a evidência de ausência.

Em lógica, a interpretação padronizada da negação é que a negação de uma fórmula é verdadeira se e somente se a fórmula é falsa. Se uma fórmula não é nem verdadeira nem falsa, sua negação é considerada desconhecida. Na interpretação da negação por falha, a negação da fórmula nesse caso é considerada verdadeira.

A negação usada em Prolog é tratada como negação por falha pelo interpretador. Se, durante o curso de execução de um programa, o interpretador tem de avaliar NOT a(B), ele tenta provar que a(B) é verdadeiro. Se essa tentativa é mal-sucedida, NOT a(B) é considerado verdadeiro.

A negação por falha é relacionada com a suposição comum de que o que não é conhecido ser verdadeiro é falso. Isso é conhecido como a Hipótese de Mundo Fechado.

Em argumentação, um ponto para o qual nenhum argumento pode ser feito é chamado um argumento infundado. Um argumento infundado para α não é um argumento fundado para a negação de α.