|
Notes:
-
The letters
O, I, and Q
are customary written in various orders, e.g.,
ALCQIO, but SHOIQ .
Here we do not reflect this tradition, but rather use a uniform naming scheme.
-
In literature, the letter F sometimes stands for
feature (dis)agreement constructor
(), rather than functionality
().
-
The presence of role intersection operator is sometimes indicated
by the letter R in literature, e.g.
ALCNR := ALCN(∩).
-
Transitive closure is usually denoted as R+.
The operators * and + are expressible from each other via
R+ = R o R* and
R* = id(T) ∪ R+.
Note however that the former definition is not linearly bounded.
Therefore, any complexity result for a logic with + immediately implies
the same result for a logic with (*,o), but not vice versa.
-
In the selector "Allow/disallow complex roles in number restriction",
a role (expression) is called complex if it contains any role operations
other than inversion (i.e. inversion is harmless (with some rare exceptions,
which are pointed out in the comments to those cases)).
However, in literature it is usually hard or even impossible to determine whether
this assumption holds by looking at the name of a logic.
For instance, ALCQIreg usually abbreviates
a logic where only role names and their inverses are allowed in number restrictions; whereas
in the logic ALCN(o),
role composition is allowed in number restrictions.
To avoid this ambiguity, the selector was introduced here explicitly.
-
In logics with unqualified number restrictions
N, one can independently allow/disallow role operations
in value restrictions (∃R.C and ∀R.C)
and/or in number restrictions (≥n R).
Therefore, strictly speaking, the naming of logics should look like
ALC(∪,—)N(∪,o).
However, in our Navigator we are only able to display logics where role constructors
are either allowed in both value and number restrictions,
or in value restrictions only. What holds for the remaining case (if known)
is usually said in comments.
Note that this this distinction is redundant for logics with qualified number
restrictions Q, since ∃R.C
can be expressed as ≥1 R.C.
-
Recall that if C is a complexity class (e.g., PSpace or ExpTime), then a problem Q is said to be
in C if there is an algorithm that belongs to the class C
and solves the problem Q (so this is an upper bound for complexity). In particular, "decidable" is
an upper bound; here C is the class of all decidable problems.
A problem Q is C-hard if all problems form the class C can be
polynomially reduced to the problem Q (so this is a lower bound;
in particular, the problem Q can be much harder, even undecidable!).
Finally, a problem Q is C-complete if it is both
C-hard and in C. For more information on
Computational Complexity Theory see [].
-
The symbol
in the above table means that the author of this web page did not find
in the literature any results concerning the corresponding logic.
If you have any information about that logic, the author would be grateful
if you send
him a mail with the referrence. Sometimes, you can find out the desired
complexity result using this tool by adding/removing some ingredients
from the logic you consider, since it is not guaranteed that whenever
this tool knows the complexity of two logics, and these complexities are the same,
then it knows the complexity of all logics in between.
As already pointed out, this tool is always
incomplete
and updated frequently.
|
