Re: TEST: complex reasoning test cases? (fwd)

------- start of forwarded message -------
From: Ian Horrocks <horrocks@cs.man.ac.uk>
To: Dan Connolly <connolly@w3.org>
Date: Fri, 14 Jun 2002 13:36:52 +0100 (BST)
Subject: Re: TEST: complex reasoning test cases?
Reply-To: Ian Horrocks <horrocks@cs.man.ac.uk>
Cc: www-webont-wg@w3.org


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

------- end of forwarded message -------