W3C home > Mailing lists > Public > www-webont-wg@w3.org > January 2003

Re: Entailments and normativity

From: Jos De_Roo <jos.deroo@agfa.com>
Date: Tue, 21 Jan 2003 14:24:24 +0100
To: "Jeremy Carroll <jjc" <jjc@hpl.hp.com>
Cc: www-webont-wg@w3.org, www-webont-wg-request@w3.org
Message-ID: <OFCCED4510.13D27387-ONC1256CB5.004969B2-C1256CB5.0049AEC2@agfa.be>

> I have made, a possibly successful, case to my HP colleagues that OWL is
> documents:
> - syntactic forms
> - semantic consistency
> The WG seemed minded to restrict our concerns to precisely those when it
> to specifying software. In particular there was no desire to specify any
> 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
> 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
> 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
> OWL Full, each of which specifies a set of RDF documents. OWL normatively
> specifies through the use of model theoretic semantics the consistency of
> such document. The model theoretic semantics also permits the discussion
> entailment relationship between pairs of documents. These relationships
> informative. In particular, implementors of OWL Consistency Checkers are
> to use alternative semantics as long as these are logically equivalent to
> OWL Consistency Checker built using the semantics specified here. No
> 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
> specification of OWL is to do with what is expected of OWL
> 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
> 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
> 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
> 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
> 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
> 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
> both the entailment and the inconsistent file are at the same OWL DL

-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Tuesday, 21 January 2003 08:29:34 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:50 UTC