- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Wed, 8 Aug 2001 06:16:41 +0100 (BST)
- To: Sandro Hawke <sandro@w3.org>
- cc: <www-rdf-logic@w3.org>
On Tue, 7 Aug 2001, Sandro Hawke wrote: > > Can anyone tell me (by rigorous analysis or rough guess) what kind of > performance characteristics I would get doing DAML reasoning using a > reasoner not built for DL? For the portion of DAML that can be > axiomatized into pure tabled prolog, does anyone know how XSB handles > it? For the rest, how otter handles it? Is it easy to tell which > territory you're in? > > -- sandro (thinking about diff'ing deductive closures) Sandro, Good results have been obtained for some related propositional modal logics using (clever) translations into FOL and the SPASS FOL prover (see work by Hustadt and Schmidt [1]). SPASS is highly configurable, and with apropriate settings it is possible to get good performance AND guarantee termination for these modal logics. With more expressive logics (like Dahl+oil), it is no longer possible to guarantee termination, e.g., in the presence of transitive properties. Ian @INCOLLECTION{HustadtSchmidt00c, AUTHOR = {Hustadt, U. and Schmidt, R. A.}, YEAR = {2000}, TITLE = {Using Resolution for Testing Modal Satisfiability and Building Models}, EDITOR = {Gent, I. P. and van Maaren, H. and Walsh, T.}, BOOKTITLE = {SAT 2000: Highlights of Satisfiability Research in the Year 2000}, SERIES = {Frontiers in Artificial Intelligence and Applications}, VOLUME = {63}, PUBLISHER = {IOS Press}, ADDRESS = {Amsterdam}, NOTE = {Also to appear in a special issue of \emph{Journal of Automated Reasoning}}, ISBN = {1 58603 061 2} }
Received on Thursday, 9 August 2001 08:39:46 UTC