Re: summary of current position with respect to semantics proposals (was Re: WOWG: agenda Aug 15 telecon)

> [...]
> 
> > I've actually redone above testcase to better reflect
> > that particular aspect of more than one ontology (*)
> >
> >   http://www.w3.org/2002/03owlt/intersectionOfP
> >   http://www.w3.org/2002/03owlt/intersectionOfX
> > OWL-entails
> >   http://www.w3.org/2002/03owlt/intersectionOfC
> 
> How?  What definition of OWL entailment did you use?  What system did 
you
> use for the test?
> 
> > using a resolution based algorithm we have
> > found the proof of that as part of the proof
> >   http://www.agfa.com/w3c/euler/etc5-proof.n3
> > (actually at the end of that file)
> 
> Ahh.  You are saying that you have a system that (conceptually) takes 
two
> sorts of input,
> 
> 1/ control input in the form of n3 statements
> 2/ a problem description in the form of n3 statements plus some other
>    information
> 
> and returns a trace showing whether the problem description is a
> consequence of the control input.
> 
> The question here is what relationships the system has to the various
> proposals for OWL entailment.  I'm not asking for a proof that the 
system
> is sound and complete wrt some proposal for OWL entailment.  A 
reasonable
> argument that the system was correct for some portions of
> some version of OWL entailment would be very useful.

well, I'm trying the RDF(S) MT extension proposal
as elaborated by DanC

> To take an easy example, and one that should be the same for all the
> proposals for OWL entailment, is there a reasonable argument to show 
that
> the system is correct, i.e., both sound and complete, for "type"
> entailments, i.e., entailments of the form
>       KB |= Q
> where KB is an OWL KB that corresponds to the abstract syntax
> and Q is a query of the form
>       i rdf:type c .
> where i appears in the KB, but not as a class or property,
> and c appears in the KB as a class.

We are incomplete.
Remember our recent discussion on this list that when given
  { ?x a :R } log:implies { ?x a [ owl:complementOf ?x ] } .
  { ?x a [ owl:complementOf ?x ] } log:implies { ?x a :R } .
we can not prove that (*)
  _:x a :R .
  _:x a [ owl:complementOf :R ] .
and while trying to do that we actually detect
some 91 cycles i.e. trying to prove something that
we are already trying to prove (aka Euler paths).

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

(*) We can argue over this, as we already did, but
we would like to keep following resolution strategies:
o depth first: each alternative is investigated until a
  unification failure occurs or until a solution is found.
o set of support: at least one parent clause must be from
  the negation of the goal or one of the descendents
  of such a goal clause.
o unit resolution: at least one parent clause must be a
  unit clause i.e. a clause containing a single literal.
o input resolution: at least one parent comes from the set
  of original clauses.
o linear resolution: the general resolution rule is followed.
o ordered resolution: the clauses are treated from the
  first to the last and each single clause is unified
  from left to right.

Received on Friday, 16 August 2002 09:12:35 UTC