W3C home > Mailing lists > Public > public-webont-comments@w3.org > August 2003

Re: soundness, completeness and decidability proofs

From: <Bernardo.Cuenca@uv.es>
Date: Thu, 28 Aug 2003 09:51:52 +0200 (CEST)
To: Christoph Mangold <Mangold@informatik.uni-stuttgart.de>
Cc: public-webont-comments@w3.org
Message-ID: <5584864821cuengrau@uv.es>



 Hi ,

  OWL-DL is considered equivalent to the SHOIN(D) description logics ( 
an extension of ALC including transitive roles, role hierarchies, 
nominals, inverse roles, unqualified number restrictiones and 
datatypes).

 A mapping can be established between OWL-DL entailment and concept 
satisfiability in SHOIN(D) and thus the decidability of OWL-DL 
entailment can be proved from the known decidability of SHOIN(D).

 For more details, there a couple of interesting papers published this 
year that provide a deep insight on these topics:

  -" From SHIQ and RDF to OWL: The Making of a Web Ontology Language"
     writen by Ian Horrocks, P.F. Patel-Schneider and F.Van Harmelen

 "Reducing OWL-entailment to Description Logic Satisfiability"
   by Ian Horrocks and P.F. Patel-Schneider

 These papers can be downloaded from Ian Horrock's web site.
 
 If you are not familiar with description logics get a copy of the 
description logics handbook.

  Viel Glück !

  Bernardo Cuenca
  Department of Computer Science
  University of Valencia


> 
> Hi,
> 
> I am new to the owl subject and I don't know if this is the 
appropriate
> place to ask my question.
> 
> As far as I understand, OWL DL is the part of OWL that enables a 
sound and
> complete inference calculus and where the entailment of statements is
> decidable. I just couldn't find any proofs for these properties of 
OWL DL.
> Can anyone give me directions?
> 
> Thanks
> Chris
> 
> -----------------
> Christoph Mangold
> 
> 
> 
Received on Thursday, 28 August 2003 03:53:28 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:43:29 GMT