Re: soundness, completeness and decidability proofs

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