- From: Enrico Franconi <franconi@cs.man.ac.uk>
- Date: Thu, 9 Aug 2001 10:30:05 +0100
- To: www-rdf-logic@w3.org
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