Negation as failure

Negation as failure is a special constrain that makes the reasoning process to fail when some conditions at runtime are verified. These constrains are expressed as rules which have the false symbol #F in the head.

In general, a Failure rule has the form: #F :- body. When the failure rule is activated (the body atoms are unified) at runtime the system will throw an exception and it will stop the reasoning process. Let us show uses with examples.

Example 1

edge(1,2).
edge(2,1).
edge(1,3).
path(X,Y):- edge(X,Y).
path(X,Z):- edge(X,Y), path(Y,Z).
#F :- path(X,X).
@output("path").

The above example computes the usual transitive closure of the binary relation edge and if the graph (described by the edge relation) contains a cycle, the failure rule is activated by throwing an exception.

Example 2

c(Id, Name) :- company(Id, Name, Revenue).
#F :- c(Id, Name1), c(Id, Name2), Name1 <> Name2.
@output("c").

The above example checks the uniqueness of the Id attribute for the company relation. When two companies have the same Id but different names then the reasoining process will fail.