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

Re: soundness, completeness and decidability proofs

From: Ian Horrocks <horrocks@cs.man.ac.uk>
Date: Thu, 28 Aug 2003 09:00:29 +0100
Message-ID: <16205.46749.741811.325076@excalibur.oaklands.net>
To: Christoph Mangold <Mangold@informatik.uni-stuttgart.de>
Cc: public-webont-comments@w3.org

On August 27, Christoph Mangold writes:
> 
> 
> 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?


The proof is by reduction to known decidable Description
Logics. Details and further pointers can be found in [1] and [2].

Ian

[1] http://www.cs.man.ac.uk/~horrocks/Publications/download/2003/HoPa03b.pdf
[2] http://www.cs.man.ac.uk/~horrocks/Publications/download/2003/HoPa03c.pdf





> 
> Thanks
> Chris
> 
> -----------------
> Christoph Mangold
> 
> 
Received on Thursday, 28 August 2003 03:53:08 GMT

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