W3C home > Mailing lists > Public > www-webont-wg@w3.org > June 2002

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

From: Ian Horrocks <horrocks@cs.man.ac.uk>
Date: Thu, 20 Jun 2002 17:53:38 +0100
Message-ID: <15634.2194.208923.100526@merlin.oaklands.net>
To: www-webont-wg@w3.org
------- 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

(defun Heinsohn-tbox-1 ()
  "Tests incoherency caused by disjoint concepts"
;Initialise (empty) ontology.
;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)
  (disjoint c d)
  (defprimconcept e3 c)
  (defprimconcept f d)
  (defprimconcept d1)
  (defprimconcept c1 d1)
  (disjoint c1 d1)
;with some reasoners it is necessary to explicitly classify the KB
;before asking any queries.
;conjoin results of 4 test queries
;should be inconsistent (obvious - they are disjoint)
   (not (satisfiable '(and c d)))
;tests inconsistency caused by a toClass restriction
   (not (satisfiable '(and (all r (and c d)) (some r *TOP*))))
;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

Regards, Ian

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

Received on Thursday, 20 June 2002 12:56:27 UTC

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