- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Mon, 12 May 2003 14:57:26 +0100
- To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
- Cc: "Jim Hendler" <hendler@cs.umd.edu>, "webont" <www-webont-wg@w3.org>
On May 12, Jeremy Carroll writes: > > > > > For some reason, the encoding of SAT problems in Test [1] uses > > nominals, rather than the standard class based encoding (e.g., as used > > in the TANCS test suite), which pushes the problem into that part of > > the language which is hard for complete reasoners to deal with. Using > > the class based encoding, FaCT is able to solve the test cases in less > > than 0.05s on a 1GHz PIII desktop. > > > > I am surprised that the failure directed backtracking techniques are not > successful on the examples I produced. I didn't say that. They may be successful in an implemented system, but I don't have access to such a system. > > They are intended to be easy for an appropriately optimized system (not that > I have an optimization to suggest - I merely ran the pre-encoded form > through a specialized reasoner, and like you got a very small time). The trouble with encoding the problem in terms of nominals is that the resulting KB is saying something much "stronger" than the original problem. In particular, there are lots of implicit cardinality constraints on the size of classes. The encoding of the problem actually relies on relatively subtle interactions between such constraints. E.g., the only reason we know that plus1 and minus1 cannot be interpreted as the same object is that the class TorF is defined to be equivalent to the class {T F}, where T and F are different, so the cardinality of TorF must be 2, so plus1 and minus1 must be interpreted as 2 different objects (phew!). Dealing with such interactions is non-trivial for a complete reasoner (and, speaking for myself, also for a human reasoner), and may rule out the use of many very useful reasoning techniques and optimisations. Having said that, the example does not use inverse roles and so would be solvable using known algorithms. For this size of problem I would expect the performance of such algorithms to be good. > > I would suggest that this report merely enhances Martin's comment. If > implementors can't implement oneOf as adequately as the rest of the language > is this going to result in confusion as to how solid OWL DL actually is? I think this is covered by Jim's proposed response. Users should be aware that nominals are a very powerful construct, and the (gratuitous) use of nominals is likely to adversely affect performance. Ian > > > Jeremy
Received on Monday, 12 May 2003 09:57:35 UTC