[DL] Re: decidability

[Bruno Woltzenlogel Paleo]

Hello Ward,

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

I think the mistake in your last question is that you associate decidability
with the query, but decidability is a property of a problem. And the
problems (satisfiability, subsumption, etc) talked about by logicians (and
loosely used by them to classify their logics as decidable or not) depend
not only on the query, but also on the whole language in which the knowledge
base is written.

To complement what Enrico Franconi explained, another very common reasoning
problem in logics in general is the validity of formulas (whether they are
true in all models). Furthermore, if we have a proof calculus for our logic,
that allow us to show formal proofs for certain formulas, we can also think
about the problem of provability (whether we can show a proof for a formula)
and its decidability. Depending on the soundness and the completeness of the
calculus, the problems of validity and provability may or may not be
equivalent. To say it slightly more precisely but still imprecisely, we are
then interested in the question: Is the formula (query) F provable/derivable
from the axioms of the theory (knowledge base and its TBox and ABox...) T
according to the rules of inference of our calculus? In other words, does F
"follow" from T? And then, is there a general algorithm that can decide this
for us for *any* F and for *any* T? It's intuitive that the existence of
such an algorithm/decision-procedure will depend on the expressiveness of
the language that we use for our F's *and* T's. The more expressive, the
less likely the existence of such a decision-procedure is.

I hope the additional example of the reasoning problem above, with a
proof-theoretical flavor, fits well your query-oriented view of the subject.
I think it also creates a link between the vocabulary usually used by DLs
(KB, TBox, ABox, query) and the vocabulary used in other logics that you
might know.

Best Regards,

------------------------------------------------------------
Bruno Woltzenlogel Paleo
Skype: bruno.wp  | Mobile: +43(680)2109403
WebSite: http://bruno-wp.blogspot.com/
WebSite: http://www.logic.at/people/bruno/