jha@lfcs.ed.ac.uk (Jamie Andrews) (12/15/89)
In article <2221@cs-spool.calgary.UUCP> cleary@cpsc.ucalgary.ca (John Cleary) gives a translation of negation into Horn clauses. This is a good try, but only works for definitions with no local variables; ie. Horn clauses in which all variables which appear in the body also appear in the head. >If p is defined as follows: > > p(X1,...) :- a11(...), ..... a1n1(....) > p(X1,...) :- a21(...), ......a2n2(....) > ... > p(X1,...) :- am1(...), ..... amnm(....) > >then np is defined as > > np(X1,...):- not(a11(...)), not(a21(...)), ... not(am1(...)) > np(X1,...):- not(a11(...)), not(a21(...)), ... not(am2(...)) > .... > np(X1,...):- not(a1n1(...)), not(a21(...)), ... not(amnm(...)) > >where each of the not(aij(..)) can be further translated or if they >are of the form not(not(q(...)) replced by q(...). [...] As an example, if we have some clauses defining the relation that X is the parent of Y: parent(X, Y) :- X = frank, Y = heather. parent(X, Y) :- X = evelyn, Y = frank. and we perform the translation, we get nparent(X, Y) :- X \= frank, X \= evelyn. nparent(X, Y) :- X \= frank, Y \= frank. nparent(X, Y) :- Y \= heather, X \= evelyn. nparent(X, Y) :- Y \= heather, Y \= frank. This is OK because nparent defines exactly the cases in which it's impossible for X to be the parent of Y. But now consider the grandparent relation: grandparent(X, Y) :- parent(X, Z), parent(Z, Y). When we perform the translation, we get: ngrandparent(X, Y) :- nparent(X, Z). ngrandparent(X, Y) :- nparent(Z, Y). But this is silly, because it's saying that X is not the grandparent of Y if X is not the parent of *some* Z. So since nparent(evelyn, heather), we have ngrandparent(evelyn, heather) by the first clause. The problem is that we have implicit existential quantifiers in the bodies of predicates. When you push a negation down through an "and" it becomes an "or", and vice versa, but when you push a negation down through an existential it becomes a universal. Your procedure pushes a negation through an existential and leaves it as an existential. Universal quantification cannot appear in the bodies of Horn clauses, unless you want to implement a full first order theorem prover; or unless you want to use some incomplete strategy, such as Lee Naish has talked about in papers and on this newsgroup. In the latter case, you're not much closer to translating negation to Horn clauses than just using negation as failure to begin with. BTW, there's nothing "non-logical" about sound negation as failure; it's just not a complete decision procedure. >The standard minimal meta-interpreter for Prolog can be extended to give this >type of behavior as follows.... This doesn't work either, for the reasons above. If it did, there'd be no problem with negation! Nice try, though... --Jamie. jha@lfcs.ed.ac.uk "Walls so thin I can almost hear them breathing"