Re: soundness, completeness and decidability proofs

 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
> 
> 
>