- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Fri, 16 Aug 2002 15:11:58 +0200
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
- Cc: www-webont-wg@w3.org
> [...] > > > 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