[Xsb-users] How to express 'forall' in XSB (as Datalog)

[David S. W. <wa...@cs...>]

Dear RLN,

I just got back from 3 weeks away and found your message, and don't
see that anyone else responded.  If they already answered your
question, then this can be ignored.

R. Lakshminarayanan writes:

 > Does any one know any similar work, that is, translation of
 > a fragment of First Order Logic into Datalog rules? or a
 > definition of the semantics of Datalog in terms of First
 > Order Logic?

The simple answer for for-all is to use the negation translation as
you suggest, and to used tnot/1 (for ``tabled not'').  This requires
that the atom being called refer to a tabled prediate.

So you can translate a forall(x,p(x) --> q(X)) to
   tnot((p(X) and tnot(q(X)))
which can be written


:- table p/1,q/1.

:- tnot(npq).
npq :- p(X), tnot(q(X)).

(If there are parameters to npq, i.e., safe variables that will be
bound in a left-to-right selection strategy, then they can be passed
to the new predicate, npq.  It works as long as all calls to tnot are
ground.) 

One warning, however.  This only works if this translation does not
introduce recursion through the negation operator, tnot.  For a single
FO formula, there will be no recursion, but if you allow FO-formulae
on the right-hand-sides of rules, then there might be recursion.  In
this case, XSB will find the well-founded model and the recursion
through negation will introduce undefined truth values, which you
probably don't want.

Regards,
-David