W3C home > Mailing lists > Public > www-webont-wg@w3.org > February 2003

TEST: harder DL tests (3 SAT)

From: Jeremy Carroll <jjc@hpl.hp.com>
Date: Fri, 28 Feb 2003 10:23:04 +0100
To: www-webont-wg@w3.org
Message-Id: <200302281023.04816.jjc@hpl.hp.com>

Sean's Tests
I have added Sean's tests - one question for Sean or Ian in
The description reads:
DL Test: t5f.1 Non-finite model example from paper The concept should be 
coherent but has no finite model
Which paper? I will add it to the references.
(These are a great addition)

OWL Lite and UnionOf

I have also added Ian's example from
which is found in 6 tests under:


I note that many of Sean's tests can be reformulated as OWL Lite tests using 
Ian's techniques, and I hope to do that (copying the tests into a new 
subsection "Harder OWL Lite Tests")

3 SAT and individuals

I was a little worried at the lack of exercise for the distinctive DL feature 
of individuals as well as classes and properties; I am also not convinced 
that Sean's tests adequately exercised the OWL DL cardinality constructs.

To partially address the first of these, I took some easy 3 SAT examples and 
formulated them in OWL DL.

I have verified these examples with zchaff:
(which solves these examples in "0" time)
I mapped the DIMACS form into OWL DL using an awk script:

I note editorially that these tests are too long for the document, and I think 
it would be better to replace the first by a very short 2 sat test with three 
clauses, and to treat the other two tests (possibly even slightly harder 
ones) in the same way as I treat the Guide examples (linked from the document 
rather than in the document).

Cardinality in OWL DL

I took the example discussed in
and added it under
I put first a simpler positive and negative case (i=2, j=3, k=5 pr k=6)
and then a harder pair of cases (i=200,j=300,k=500 or k=600)

Philoshophy of Harder DL Tests
I would like the harder tests to be pitched at a level for which:
- naive implementations will not solve them
- competent but uninspired implementations will solve them over a cup of 
coffee (or lunch)
- inspired implementations can solve them in milliseconds

Received on Friday, 28 February 2003 04:22:53 UTC

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