Re: CR/PR questions

OWL DL seems to differ from OWL Lite in two important respects:
1) it allows unnamed descriptions and the full remit of set theoretic 
constructions

2) it has the owl:oneOf and owl:hasValue constructions, and hence finite 
classes

3) higher cardinalities, which interact with finite classes in interesting 
ways.

The first seems trivial from an implementation point of view: these things can 
be converted into OWL Lite.

However the second seems to permit a wide range of axioms that are not wdiely 
used in DAML+OIL experience nor over which there seems to be much real 
practical experience of reasoning.

In the TEST editors draft at the moment we have some 3-SAT tests

http://www.w3.org/2002/03owlt/editors-draft/draft/proposed-dl-500-SAT

these are, from a specialist 3-SAT reasoner point of view trivial, (i.e. they 
solve in less than a second) but not ones for which I expect a queue of OWL 
implementations

I am working on expressing some of the Venn diagram problems I have worked on 
in OWL, for instance, the attached picture can be described in OWL DL to a 
surprising degree of accuracy (e.g. its vennness, i.e. there are 5 
overlapping shapes giving 32 distinct regions, the triangularness, in terms 
of 15 intersecting pseudolines etc).

These descriptions depend on giving multiple names to the same geometric 
object (face, edge, line, point), and leaving the reasoner to sort out the 
tangle.

On cardinality, it is possible to embed substantial portions of arithmetic 
within OWL DL, and a practical reasoner intending to process this language 
should be aware of cardinality.
 
Ian reported having successfully completed the addition tests 901 thru 904

http://www.w3.org/2002/03owlt/editors-draft/draft/proposed-dl-900-arith#proposed-dl-900-arith

however, his reasoner is currently doing this long hand and he had to leave it 
running overnight to work out that 200+300 != 600 because the numbers are 
large.

I am not compelled that Ian will manage when I ask him if 200*300=60000

Jeremy