Re: Semantic Web Rule Language (SWRL) 0.5 released

   [me]
   I have some trouble understanding the RuleML web site.  There are so
   many alternatives syntaxes.  Is one of them, or are some of them,
   "official"?  (This is an embarrassing admission for me to make since
   I'm listed on the website as a participant.)

   [Harold Boley]
   The "official" version is always the newest release linked at
   http://www.ruleml.org/#DTDs-Schemas.
   The RuleML DTD Version 0.8 has been quite stable for some time.
   A RuleML DTD+Schema Version 0.85 with 'roles' from OO will hopefully be
   released by 19 Dec, solving a long-standing XML Schema inheritance problem
   (http://www.ruleml.org/inxsd0.8.html#Issues).

I have taken another look, and I'm still baffled.  The link you
specify leads to http://www.ruleml.org/indtd0.8.html, and from there
you are directed to a maze of twisty passages.  Eventually you stumble
upon the tree that shows the relationships among all the possible
syntaxes for RuleML.  Ah!  The example T3/X3 is said to be the 0.8
version of the example rule.  But where is the DTD or schema for the
language of which this rule is an exemplar?

   [me]
   But the argument list in Lisp 'defun' _is_ a quantifier; it
   establishes a scope for variables as surely as 'lambda' does.

   [Harold]
   Yes, by (top-level) convention. Similarly, your modified Example 6.1-2 in
   http://lists.w3.org/Archives/Public/www-rdf-rules/2003Nov/0178.html
   (where your embedded <ruleml:Imp> should be called <ruleml:Implies>)
   by (top-level) convention becomes the original Example 6.1-2 in
   http://www.daml.org/rules/proposal/rdfsyntax.html
   (since <ruleml:Imp> establishes a variable scope like <drs:Forall> does).

No!  There is a big difference between an implicit top-level scope and
the scope established by some kind of explicit binder (such as
'defun', 'lambda', or 'forall').  The difference appears when the
expression is embedded in another expression.  Consider the case of E,
an expression with no free variables, and F, an expression with one or
more free variables.  (not E) is true whenever E is false, by the
usual semantics of 'not'.  But this is not so for (not F); the
top-level convention changes the scope of the free variables to
include the 'not'.  If F is (if (P ?x) (Q ?x)), then (not (if (P ?x)
(Q ?x))) means that for all x, (P x) is true and (Q x) is false.  

If you eliminate explicit existentials by premature skolemization, you
get a whole different class of distortions.

The moral is that the normal form used by resolution should be applied
at the last minute, before the search for a proof begins.  Prior to
that, retain the explicit binders.  

   [Harold]
   But again, I think we should put a version of your (DRS) suggestion into
   the SWRL (and RuleML, ...) issues lists.

I won't object!

                                             -- Drew

Received on Tuesday, 2 December 2003 13:23:22 UTC