Negation as failure

It is essentially a Horn clause theorem prover augmented with a special inference rule for'dealing with