[DL] decidability
Enrico Franconi
franconi at inf.unibz.it
Fri Dec 28 10:35:01 CET 2007
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/
> . **
More information about the dl
mailing list