[DL] decidability

[Enrico Franconi]

As you point out, given a logic, a reasoning problem (like  
satisfiablity of concepts, subsumption between concepts, or knowledge  
base satisfiability) may be or may be not decidable. For expressive  
logics all the above standard reasoning problems are mutually  
reducible, and specifically they are reducible into KB satisfiability,  
which is used as the reference problem for the logic. So, with some  
degree of imprecision, we may generically say that a DL is undecidable  
if its KB sat problem is undecidable. Given a logic, in order to prove  
undecidability of its KB sat problem (and therefore of all of its  
standard reasoning problems), usually you provide the encoding of each  
instance of an already known undecidable problem (e.g., some tiling  
problem) in a corresponding KB sat instance (i.e., an ontology) which  
is satisfable if and only if the corresponding instance of the  
undecidable problem has a solution.
cheers
--e.

On 18 Dec 2007, at 13:07, Ward wrote:

> Dear all,
>
> I am trying to understand more of Description Logics and I have a  
> question about decidability. If I understand it right then  
> decidability was originally only used for problems or queries or  
> something like the satisfiability of a class. Now a logic language  
> is called 'undecidable' if it is possible to construct an ontology  
> with it, about which you can pose undecidable questions.
> What does it mean for a logic language to be undecidable? Is it a  
> bad language? Is it not the task of a reasoner to point out whether  
> a query is decidable, instead of restricting the whole language?
>
> Thank you very much,
>
> Ward
> ---
> **  You received this mail via the description logic mailing list;  
> for more  **
> **  information, visit the description logic homepage at http://dl.kr.org/ 
> .  **