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

On August 7, Sandro Hawke writes:
> 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?

Few years ago there was some debate in the DL community about the
feasibility of the translation to a FOL prover approach. There are a
number of interesting publications, a freely available prover based on
the translation into FOL idea, and even a WWW accessible interface for
it.  Check this at <http://www.cs.man.ac.uk/~schmidt/mspass/>.

The following publication can be used as a starting point:


@INPROCEEDINGS{HustadtSchmidt00b,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
YEAR = {2000},
TITLE = {{MSPASS}: Modal Reasoning by Translation and First-Order Resolution},
EDITOR = {Dyckhoff, R.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX 2000)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1847},
PUBLISHER = {Springer},
PAGES = {67--71},
ISBN = {3-540-67697-X},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtSchmidt00b.html},
ABSTRACT = {\textsc{mspass} is an extension of the first-order theorem
prover \textsc{spass},
which can be used as a modal logic theorem prover, a theorem prover for
description logics and a theorem prover for the relational calculus.
}
}

cheers
-- e.

Enrico Franconi                     - franconi@cs.man.ac.uk
University of Manchester            - http://www.cs.man.ac.uk/~franconi/
Department of Computer Science      - Phone: +44 (161) 275 6170
Manchester M13 9PL, UK              - Fax:   +44 (161) 275 6204

Received on Thursday, 9 August 2001 05:33:06 UTC