Tests

Jeremy,

Some preliminary comments on Test:


1. An awful lot of test are in OWL Full. It would make sense, wouldn't
it, to at least have DL/Lite versions of those tests that could
easily be rendered in DL/Lite (all be it with some extra information)
- particularly given that most of the immediately available
implementations are of DL/Lite. In many cases all that is required is
fixing the type of various components of the test, i.e., owl classes,
object properties, etc.


2. Sean's species validator says that <disjointWith/conclusions001> is
Lite. It looks like Lite to me too.


3. The species validator says that <equivalentClass/conclusions001> is
not in itself Lite because Automobile and Car are not typed. This does
seem to be true - the ontology is in fact in Full. I'm not sure if it
is the intention that the "Lite" in this case refers to the ontology
on its own or in conjunction with the premise ontology.


4. Two more suggested intersectionOf tests:

   sameClassAs(intersectionOf(C owl:Thing) D) |= sameClassAs(C D)
   sameClassAs(intersectionOf(C owl:Nothing) D) |= sameClassAs(D owl:Nothing)

   Similarly for unionOf:

   sameClassAs(unionOf(C owl:Thing) D) |= sameClassAs(D owl:Thing)
   sameClassAs(unionOf(C owl:Nothing) D) |= sameClassAs(C D)


5. I checked:

<cardinality/Manifest001#test> 
<cardinality/Manifest002#test> 
<cardinality/Manifest003#test> 
<cardinality/Manifest004#test> 

using a combination of the species validator and FaCT reasoner (I used
the validator to translate to abstract syntax and then the FaCT
reasoner to check the entailment w.r.t. the abstract syntax). FaCT had
no difficulty in proving this entailment. The validator barfs on
<cardinality/Manifest005#test> (which is full, so I wouldn't have been
able to check it with FaCT in any case).


6. I checked:

<equivalentClass/Manifest006#test>
<I5.2/Manifest001#test>
<I5.2/Manifest002#test>

via the same mechanism.


7. The entailment test:

<description-logic/Manifest901#test>

was successful, but not for the reasons you intend. You have domain
constraints in the premises when they should be range. The result is
that the class:

intersectionOf(restriction(a-q minCardinality(3)) 
               restriction(a-p minCardinality(2)))

is equivalent to owl:Nothing, and so is a subClassOf every class. With
the domains changed to ranges the entailment still holds because of the
cardinality interactions you were interested in.

For the same reason, the test:

<description-logic/Manifest902#test>

fails - i.e. the entailment holds. It no longer holds when domain is
changed to range.

Similarly for tests <description-logic/Manifest903#test> and
<description-logic/Manifest904#test>. (I wasn't able to prove the
corrected version of 903 yet due to the large numbers - I will run it
overnight and see what happens. It is interesting to note that well
known optimisations for non-qualified CRs should deal with this
trivially, but FaCT treats everything like a QCR with owl:Thing as the
qualifier.)


8. I am starting to work my way through the "Extended Satisfiability
Tests", but it is quite time-consuming. So far I have checked:

<description-logic/Manifest001#test>
<description-logic/Manifest002#test>
<description-logic/Manifest003#test>
<description-logic/Manifest004#test>
<description-logic/Manifest005#test>

<description-logic/Manifest105#test>
<description-logic/Manifest106#test>

<description-logic/Manifest901#test>
<description-logic/Manifest902#test>
<description-logic/Manifest903#test>
<description-logic/Manifest904#test>


Regards, Ian

Received on Tuesday, 29 April 2003 13:47:53 UTC