Why there is forward chaining inference engine (reasoner) for description logics only and not for other logics?

Question

Reasoner is forward chaining inference engine (https://en.wikipedia.org/wiki/Semantic_reasoner) as opposite to Prolog backward chaining SAT solver (for queries). Why there is reasoner for description logics and not for other logics?

Answer 1

This question is a bit strange. I see it's based on the Wikipedia article, but that article is also a bit strange. I will try to clarify some concepts.

---

First, we have a language that can be used to make claims whose meaning are formally defined. Such a language may allow us to say, for example, that if $x$ is a Person, then $x$ is a Human, which can be done in first order logic as $\forall x (\neg\mathsf{Person}(x) \vee\mathsf{Human}(x))$, in a rule language like Datalog as $\mathsf{Person}(x) \rightarrow \mathsf{Human}(x)$, in description logics as $\mathsf{Person} \sqsubseteq \mathsf{Human}$ and so forth.

Second, we have semantics, which formally defines the meaning of claims in the language. One way in which the semantics of a language can be defined is using model theory, which essentially maps terms in the language to sets, elements, and relations between sets; for example, we can map the term $\mathsf{Person}$ to a (hypothetical) set $P$ and $\mathsf{Human}$ to a (hypothetical) set $H$, and define the above claims as formally meaning $P \subseteq H$. This gives rise to the notion of models, where for example, $P := \{ \mathrm{Fred}, \mathrm{Jill} \}$ and $H := \{ \mathrm{Fred}, \mathrm{Jill}, \mathrm{Tom} \}$ is a model satisfying a given set of formal claims (since $P \subseteq H$), while $P := \{ \mathrm{Fred}, \mathrm{Tom} \}$ and $H := \{ \mathrm{Fred}, \mathrm{Jill} \}$ is not a model (since $P \not\subseteq Q$). In turn, models give rise to entailment between sets of formal claims, where for example, given $\{ \mathsf{Person}(\mathrm{Tom}), \mathsf{Person} \sqsubseteq \mathsf{Human} \}$ (in whatever language), we know this entails $\{ \mathsf{Human}(\mathrm{Tom}) \}$ as any model of the former set of claims must be a model of the latter set of claims.

Third, we have reasoning procedures to decide entailment. One way in which this is done is to use inference rules. For example, we may derive a rule such as $(\mathsf{C} \sqsubseteq \mathsf{D} \wedge \mathsf{C}(x)) \rightarrow \mathsf{D}(x)$ to support reasoning with respect to the $\sqsubseteq$ operator in description logics. This rule may be applied for forward-chaining or backward-chaining. But there are many forms of reasoning procedures suitable for different types of languages; for example, for more expressive description logics, (a finite set of Horn) rules is not sufficient to guarantee complete reasoning, and so tableau-based methods are often used. Also one reasoning procedure can be useful for reasoning in different languages, where Datalog, for example, is natively based on rules.

---

Returning to the question:

Reasoner is forward chaining inference engine (https://en.wikipedia.org/wiki/Semantic_reasoner) as opposite to Prolog backward chaining SAT solver (for queries).

A "reasoner" can adopt multiple strategies, including, but not limited to, forward-chaining on rules. Engines that apply tableau-based methods, backward chaining, resolution, etc., are also "reasoners". (The article you base the question on never claims that reasoners are forward chaining rule engines, but mentions this as one strategy.)

Why there is reasoner for description logics and not for other logics?

There are reasoners for other logics. For example, Vampire is a reasoner for first-order logic, XSB is a reasoner for Prolog, or just check here for a list of different reasoners for different languages.

Answer 2

Section 9.3.2 of the leading artificial intelligence textbook contains a sketch implementation of a forward chaining inference engine.