Re: Doing description logics (DAML) inference as FOL (eg using otter)

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