Entailments and normativity

I have made, a possibly successful, case to my HP colleagues that OWL is about 
documents:
- syntactic forms
- semantic consistency

The WG seemed minded to restrict our concerns to precisely those when it came 
to specifying software. In particular there was no desire to specify any more 
complicated reasoning component, such as one that could actually run our 
entailment tests.

So we have:
- a semantics that permits discussion of the meaning of a single document 
(specifically its consistency)
- a semantics that permits discussion of the relationship between two 
documents (entailment)
- three syntactic levels

What I have heard we want to have as CR exit criteria is adequate exploration 
of the first and third of these; and not much on the second.

This could possible be better reflected by making the entailment part of the 
semantics informative rather than normative.

Possible text near the beginning of the AS&S:
[[
OWL specifies an RDF vocabulary and three syntactic levels: OWL Lite, OWL DL, 
OWL Full, each of which specifies a set of RDF documents. OWL normatively 
specifies through the use of model theoretic semantics the consistency of any 
such document. The model theoretic semantics also permits the discussion of 
entailment relationship between pairs of documents. These relationships are 
informative. In particular, implementors of OWL Consistency Checkers are free 
to use alternative semantics as long as these are logically equivalent to an 
OWL Consistency Checker built using the semantics specified here. No other 
constraints on the semantics of OWL implementations are normatively 
specified.
]]

(with appropriate 'normative' and 'informative' markers elsewhere)

The motivation here is that much of the difficulty HP has with the current 
specification of OWL is to do with what is expected of OWL implementations, 
and an apparent mismatch between that and the sketch of CR exit criteria 
created at the f2f. Specifically we do not intend to migrate Jena to the OWL 
Semantics any time soon, nor do we see competing systems planning such a 
migration either; nor do we see a WG intending to make the migration of such 
a system to OWL (and its semantics) a CR exit criterion.

To give a specific example, the comprehension principle is part of OWL 
semantics, i.e. that various classes and restrictions necessarily exist. 
These can be turned into consistency tests at the OWL Full level but not at 
OWL DL or OWL Lite. e.g.

<owl:Restricition>
  <owl:onProperty>
     <owl:ObjectProperty rdf:ID="p"/>
  </owl:onProperty>
  <owl:hasValue>
      <owl:Thing rdf:ID="v"/>
   </owl:hasValue>
   <rdf:type>
      <owl:Class>
         <owl:complementOf rdf:resource="&owl;Class"/>
      </owl:Class>
   </rdf:type>
</owl:Restriction>

This says that a particularly restriction is not an OWL Class, and this is 
inconsistent. 
This:
(a) seems plausibly straight forward to implement (I wouldn't be surprised if 
Euler already could prove this)
(b) is anyway in OWL Full where we are being explicit about the lower 
implementability goals.

The alternative OWL DL entailment:

<owl:ObjectProperty rdf:ID="p"/>
<owl:Thing rdf:ID="v"/>

DL-entails

<owl:Restricition>
  <owl:onProperty>
     <owl:ObjectProperty rdf:ID="p"/>
  </owl:onProperty>
  <owl:hasValue>
      <owl:Thing rdf:ID="v"/>
   </owl:hasValue>
</owl:Restriction>

seems to present more difficulty, particularly in a forward chaining 
environment, and the WG does not seem minded to want to see even one complete 
OWL DL reasoner that could do this before exiting CR.

(I note that a unionOf example would be a lot less compelling, partly because 
both the entailment and the inconsistent file are at the same OWL DL level)

Jeremy

Received on Tuesday, 21 January 2003 05:14:40 UTC