What is supported in First Order Logics which is not supported in Description Logic?

Question

While studying description logics (DL), it is very common to read that it is a fragment of first order logics (FOL), but it is hard to read something explicitely on what is excluded from DL which is part of FOL, which makes DL (with all its dialects ALC, SHOIN etc...) decidable. Or in another words, could you provide me some examples in FOL which are not expressible through DL (and which are the reason for semi/non-decidability in FOL) ?

Deplorable

This is an interesting question, but it's really too broad for the Stack Overflow format ("There are either too many possible answers, or good answers would be too long for this format.") It might be a better fit on answers.semanticweb.com, but I suspect that there are already plenty of answers out there on the web. – Junta

As a very simple example, you can't do most things that require more than two variables in DLs. E.g., you can't describe the class of people that like someone that like someone else that like the original person, whereas it's easy in FOL: ∀x.(C(X) ↔ ∃y.(likes(x,y) ∧ ∃z.(likes(y,z) ∧ likes(z,x)))). – Junta

As another example, you typically can't express "agreement of properties" in DLs. You can't talk about the class of people whose first grade teachers are also their favorite teachers, but it's easy in FOL: ∀x.(C(x) ↔ ∃z.(favoriteTeacher(x,z) ∧ firstGradeTeacherOf(x,z))). – Junta

Thanks Joshua, those are nice examples! So it seems, whenever one variable is bound and used in more than one property it gets difficult in DL ... – Deplorable

No, that's not an accurate description. Look at the axiom "Child ⊑ ∃hasFather ⊓ ∃hasMother." It corresponds to the FOL formula "∀x.(Child(x) ↔ (∃y.hasFather(x,y) ∧ ∃y.hasMother(x,y)))" which uses the variable x with multiple properties. – Junta

Alright, so it's bascially using more than 2 (bound) variables which is not expressible in DL !? – Deplorable

For the older DL constructs, that's often true, but you can do things in DLs that require more variables. E.g., if you declare a property transitive, then you're saying "∀x,y,z.(p(x,y) ∧ p(y,z) → p(x,z))", and that requires three. In OWL 2 you can also do subproperty chains, which means, essentially, ∀w,x,y,z.(p(w,x) ∧ q(x,y) ∧ r(y,z) → s(w,z)). That also can require more than two variables. It's not as simple as "how many variables does it take?" And DLs can do some things that you can't do in FOL, like transitive closure of roles. – Junta

Answer 1

The following facts about description logics are closely related to decidability:

1. (a form of) tree-model property — this property is important for tableu methods;
2. embeddability into multimodal systems — which are known to be "robustly decidable";
3. embeddability into the so-called guarded fragments of FOL — see below;
4. embeddability into two-variables FOL fragments — which are decidable;
5. locality — see below.

Some of these facts are syntactical, while some are semantical. Here below are two interesting, decidability-related, and more or less syntactical characteristics of description logics:

Locality (from The Description Logic Handbook, 2nd edition, section 3.6):

One of the main reasons why satisfiability and subsumption in many Description Logics are decidable – although highly complex – is that most of the concept constructors can express only local properties about an element 〈...〉 Intuitively, this implies that a constraint regarding x will not “talk about” elements which are arbitrarily far (w.r.t. role links) from x. This also means that in ALC, and in many Description Logics, an assertion on an individual cannot state properties about a whole structure satisfying it. However, not every Description Logic satisfies locality.

Guarded fragment (from The Description Logic Handbook, 2nd edition, section 4.2.3)

Guarded fragments are obtained from first-order logic by allowing the use of quantified variables only if these variables are guarded by appropriate atoms before they are used in the body of a formula. More precisely, quantifiers are restricted to appear only in the form
     ∃y(P(x,y) ∧ Φ(y))         or      ∀y(P(x,y) ⊃ Φ(y))               (First Guarded Fragment)
     ∃y(P(x,y) ∧ Φ(x,y))      or      ∀y(P(x,y) ⊃ Φ(x,y))            (Guarded Fragment)
for atoms P, vectors of variables x and y and (first) guarded fragment formulae Φ with free variables in y and x (resp. in y).

From these points of view, analyze the examples from @JoshuaTaylor's comments:

• ∀x.(C(X) ↔ ∃y.(likes(x,y) ∧ ∃z.(likes(y,z) ∧ likes(z,x))))
• ∀x.(C(x) ↔ ∃z.(favoriteTeacher(x,z) ∧ firstGradeTeacherOf(x,z)))

---

The reasons why DL is preferred to FOL for knowledge representation are not only decidability or computational complexity related. Look at the slide called "FOL as Semantic Web Language?" in this lecture.

Marrin

Answer 2

As shown by Turing and Church, FOL is undecidable, because there is no algorithm for deciding if a FOL formula is valid. Many description logics are decidable fragments of first-order logic, however, some description logics have more features than FOL, and many spatial, temporal, and fuzzy description logics are undecidable as well.

Nariko