- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Fri, 14 Jun 2002 13:36:52 +0100 (BST)
- To: Dan Connolly <connolly@w3.org>
- Cc: www-webont-wg@w3.org
- Message-ID: <15625.58212.464820.663340@excalibur.oaklands.net>
On June 6, Dan Connolly writes: > > On Thu, 2002-06-06 at 04:27, Ian Horrocks wrote: > > > > Up to now, all the "official" test cases I have seen involve > > relatively trivial reasoning, usually about named individuals. E.g.: > > > > [ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] . > > > > Are we going to have test cases that involve more complex entailments, > > e.g., involving equivalent class expressions? > > If you provide them, we will. > > > Some time ago I > > submitted a whole set of examples of such test cases, many of which > > are carefully designed so to test the correctness of implementations. > > You gave a pointer to some files; I looked at translating them > to DAML+OIL, but I couldn't understand them. Fair enough - I guess they are a bit cryptic. The examples are taken from papers, are test cases that I have devised, or demonstrate bugs that were found (and fixed!) in FaCT and/or other DL reasoners. They are all of the same form: lisp functions that should return T if everything works according to spec. In general they set up an ontology and then ask one or more queries (conjoining the answers of multiple tests). I have annotated below the first test (taken from Heinsohn et al., AI 68 (1994) pp367-397), which should hopefully make everything clear: (defun Heinsohn-tbox-1 () "Tests incoherency caused by disjoint concepts" ;Initialise (empty) ontology. (init-tkb) ;There are 2 kinds of concept axiom: defprimconcept and ;defconcept. The former is equivalent to subClassOf and the latter to ;sameClassAs. Both take 2 parameters, C1 and C2. In defprimconcept C2 ;is optional - if omitted, Top (Thing) is assumed. ; ;First we introduce 2 concept (class) names c and d with no description ;(i.e., subClassOf Thing), and a role (property) name . ;Not required in D+O, but some DL systems insist on names being "typed". (defprimconcept c) (defprimconcept d) (defprimrole r) ;disjointWith(c,d) (disjoint c d) ;subClassOf(e3,C) (defprimconcept e3 c) ;subClassOf(f,d) (defprimconcept f d) ;subClassOf(d1,Thing) (defprimconcept d1) ;subClassOf(c1,d1) (defprimconcept c1 d1) ;disjointWith(c1,d1) (disjoint c1 d1) ;with some reasoners it is necessary to explicitly classify the KB ;before asking any queries. ;(classify-tkb) ;conjoin results of 4 test queries (and ;intersectionOf(c,d) ;should be inconsistent (obvious - they are disjoint) (not (satisfiable '(and c d))) ;intersectionOf(toClass(r,intersectionOf(c,d)),hasClass(r,Thing)) ;tests inconsistency caused by a toClass restriction (not (satisfiable '(and (all r (and c d)) (some r *TOP*)))) ;intersectionOf(e3,f) ;tests inconsistency of subclasses of disjoint classes (not (satisfiable '(and e3 f))) ;c1 should be inconsistent - it is a subclass of a class it is disjoint with (not (satisfiable 'c1)))) Attached is a DAML+OIL ontology where the classes t1-t4 correspond to the above 4 tests and are therefore all be inconsistent (c1 is of course also inconsistent). I created the ontology with OilEd and tested it with FaCT (which gives the expected result). Let me know if you still have problems understanding the other test cases. Regards, Ian
> > > > > Ian > -- > Dan Connolly, W3C http://www.w3.org/People/Connolly/ >
Attachments
- application/octet-stream attachment: heinsohn1.daml
Received on Friday, 14 June 2002 11:40:52 UTC