- From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- Date: Mon, 12 May 2003 13:57:53 +0200
- To: "Ian Horrocks" <horrocks@cs.man.ac.uk>, "Jim Hendler" <hendler@cs.umd.edu>
- Cc: "webont" <www-webont-wg@w3.org>
> > 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. 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). 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? Jeremy
Received on Monday, 12 May 2003 07:58:20 UTC