problematic literal-related rules of OWL 2 RL

Hi!

I know this comes very late in the process, but I want to state it anyway, after having had a private discussion on this topic with Ivan and Zhe this month. 

While creating the datatype related testcases of the RL-specific fraction of my testsuite (/not/ in the WG-approved subset of testcases) and playing around with implementing RL reasoning, I started to consider several of the rules in Table 8 of the RL specification (Section 4.3 of Profiles) to be problematic, e.g. rule: 

  <http://www.w3.org/2007/OWL/wiki/Profiles#dt-diff>

The RL rules generally do not introduce new nodes such as bNodes in the consequent, when it isn't already in the premise. This "principle" contributes to the simplicity of the language. But the rules "dt-type2", "dt-eq" and "dt-diff" in Table 8 are different. For example, rule "dt-diff" states that

  FORALL literals lt1 and lt2 with different data value:
      IF
          /* nothing */
      THEN
          T(lt1, owl:differentFrom, lt2) 

This leads to infinitely many triples even when starting from the empty RDF graph. For example, via this rule the following entailment holds for RL:

  (*) {} |= { "42"^^xsd:integer owl:differentFrom "21.0"^^xsd:decimal . }   

This is very different from, for example, the reflexivity rule for owl:sameAs, which only "fires" for nodes that exist in the original graph. I think that these rules in Table 8 significantly add to the complexity of the OWL 2 RL/RDF ruleset, and in this form the usefulness as a "starting point for practical implementation using rule-based technologies" is IMHO much reduced.

My suggestion would be to weaken the rules "dt-type2", "dt-eq" and "dt-diff" in a way that literals on the right hand side must occur on the left hand side of the rules. So, (*) would no longer follow from the RL rules, but (**) would still be a valid conclusion:

  (**) { 
         ex:s1 ex:p1 "42"^^xsd:integer . 
         ex:s2 ex:p2 "21.0"^^xsd:decimal . 
       } 
       |= 
       { "42"^^xsd:integer owl:differentFrom "42.0"^^xsd:decimal . }

But this wouldn't be a big problem anymore, since there would then only be a finite set of conclusions from the premise graph.

AFAICT, this change would also need to be propagated to theorem PR1. Take for example the following entailment query:

  (***) { ex:s ex:p "42"^^xsd:integer . }
        |= 
        { ex:s ex:p "42.0"^^xsd:decimal . }

This actually follows from the current OWL 2 RL/RDF rules because of rule "dt-eq", via an "intermediate" owl:sameAs triple between "42"^^xsd:integer and "42.0"^^xsd:decimal (and via the substitution rule for owl:sameAs). It also follows from the Direct Semantics and, AFAICT, (***) satisfies the conditions of PR1. But (***) would not follow by the weakened version of rule "dt-eq", since the literal "42.0"^^xsd:decimal is not mentioned on the left hand side.

What's your opinion on this last minute change request?

Regards,
Michael

--
Dipl.-Inform. Michael Schneider
Research Scientist, Dept. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: michael.schneider@fzi.de
WWW  : http://www.fzi.de/michael.schneider
=======================================================================
FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts, Az 14-0563.1, RP Karlsruhe
Vorstand: Prof. Dr.-Ing. Rüdiger Dillmann, Dipl. Wi.-Ing. Michael Flor,
Prof. Dr. Dr. h.c. Wolffried Stucky, Prof. Dr. Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus
=======================================================================