Negation as failure

Negation as failure (NAF, for short) is a non-monotonic inference rule in logic programming, used to derive ${\displaystyle \mathrm {not} ~p}$ (i.e. that ${\displaystyle ~p}$ is assumed not to hold) from failure to derive ${\displaystyle ~p}$. Note that ${\displaystyle \mathrm {not} ~p}$ can be different from the statement ${\displaystyle \neg p}$ of the logical negation of ${\displaystyle ~p}$, depending on the completeness of the inference algorithm and thus also on the formal logic system.

...
Wikipedia