[DL] question: complex role inclusion axioms

[Franz Baader]

Actually, both the question asked by Davide and the answers given
so far need some clarification. First of all, what properties of DLs with
complex inclusion axioms of the form R \bullet S \sqsubseteq Q
are you interested in?

If it is decidability/complexity, then there is a problem in expressive DLs
(actually, already in ALC and even some sublanguages). Satisfiability and
subsumption are then UNDECIDABLE. The papers by Uli, Ian and others that
show decidability do this under an additional restriction: the role inclusion
axioms must satisfy some acyclicity condition.

Without such acyclicity restrictions, you have decidability in certain
extensions
of EL (see our IJCAI'05 paper "Pushing the EL Envelope", which can be found
on our publication Web page  http://lat.inf.tu-dresden.de/research/papers.html).

Regarding the addition of axioms

    [Q]p \rightarrow [R][S]p

to a logic (say PDL or ALC): for which p do you want to do this?
If this is an axiome scheme (i.e., p can be replaced by all formulae),
then this may be a valid axiomatization of say ALC with role inclusion axioms
(if you add the scheme to the axioms for K). But this adds infinitely
many axioms,
so there is no direct consequence for decidability. In fact, we know
undecidability!
Thus, the usual approach to restrict the instantiations of p to the subformulae
of the formula whose satisfiability we want to decide does not work. And anyway,
I am not even sure that the axiomatization (with all instances) is really
complete for arbitrary sets of complex role inclusions (for papers that
look at such questions you should look at papers on so-called "grammar
logics", e.g. by Stephane Demri).

Best regards,

-Franz

On 9/22/06, davide <davide at cs.uu.nl> wrote:
> I have been looking in the literature for DLs enabling role hierarchies
> including comlex inclusion axioms such as, for instance:
> R \bullet S \sqsubseteq Q (the composition of R and S is a sub-role of Q).
>
> For DLs as expressive as Dynamic logic (or some relevant fragments) this
> shouldn't be anything problematic since such axioms seem to be
> translatable in  Dynamic logic. For instance:
> [Q]p \rightarrow [R][S]p
>
> Is this a correct intuition? Are there any references systematically
> adressing the issue of complex role inclusions?
> Thanks a lot for your attention.
>
> Davide
>
> --
> ===============================================
> Davide Grossi
> Intelligent Systems Group
> Institute of Information and Computing Sciences
> Universiteit Utrecht
> phone : +31 - 30 - 253 4432
> fax   : +31 - 30 - 251 3791
> http://www.cs.uu.nl/staff/davide.html
> ===============================================
>
> ---
> **  You received this mail via the description logic mailing list; for more  **
> **  information, visit the description logic homepage at http://dl.kr.org/.  **
>
>