Re: 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.


I don't see why, but I read further...


> 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.


hm.. is certainly a reasonable step for the roadmap
and above "second" could be a second step
my experience though is that e.g. proving
inconsistencies is not easier than the "second"


> 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)


well, we now can...

 {
  <http://www.agfa.com/w3c/euler/owl-rules#rule20c2> .
  _:905719_1 owl:complementOf owl:Class.
  _:905719_1 a owl:Class} log:implies
{_:905719_1 log:inconsistentWith owl:complementOf}.


> (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.


right, I don't know how to solve that one and I also note that
all our 7 "no proof found" ones have to do with lack of comprehesion


> (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)


-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Tuesday, 21 January 2003 08:29:34 UTC