TEST: harder DL tests (3 SAT)

Sean's Tests
==========
I have added Sean's tests - one question for Sean or Ian in
http://www.w3.org/2002/03owlt/editors-draft/snapshot#dl-000-satisfiability-025
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
http://lists.w3.org/Archives/Public/www-webont-wg/2003Jan/0401.html
which is found in 6 tests under:

http://www.w3.org/2002/03owlt/editors-draft/snapshot#proposedIssue-I5.2-Language-Compliance-Levels

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.
http://www.w3.org/2002/03owlt/editors-draft/snapshot#proposed-dl-500-SAT

I have verified these examples with zchaff:
http://ee.princeton.edu/~chaff/zchaff.php
(which solves these examples in "0" time)
I mapped the DIMACS form into OWL DL using an awk script:
http://www.w3.org/2002/03owlt/bin/2owlA.awk

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
http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/0211.html
and added it under
http://www.w3.org/2002/03owlt/editors-draft/snapshot#proposed-dl-900-arith
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

Jeremy

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