The Inference of Knowledge via Description Logic is a problem of Decidability. All the Inference problems must be solved in a finite time, so they must be decidable.
For Description Logics which are Fragments of First Order Logics in Principle we can apply all the algorithms, like Resolution or Tableaux, but the Problem is if we apply on Description Logics the Algorithms from First Order Logic then the Algorithm possible do not terminate, because for First Order Logic is only semi-decidable, because some Algorithm do not terminate and one does not know if they terminate.
The Problem with Description Logics is that we have to find Algorithms that always terminate and there might be not "naive" solutions. So one has to adapt the Algorithm from First Order Logic and apply them on Description Logics and maintain the Property that they will terminate and therefore are decidable. So e one has to adapt the First Order Inference Algorithms to the Properties of Description Logics.
For the Tableaux Algorithm and also for Resolution one shows the unsatisfiability of a Knowledge Base or a Theory. Therefore one does an Adaption to the Entailment Problems to the **detection of Contradiction in the Knowledge Base which means one tries to proof the Unsatisfiability of the Knowledge Base.
The Inference Problems need to be transformed in order to proof the unsatisfiability or the Detection of Contradictions, based on the Problem we are considering.
for each inference Problem there always exists and Algorithm that terminates in finite time
Description Logics are Fragments of First Order Logic, therefore (in principle) FOR Inference Algorithm (Resolution, Tableaux) can be applied.
But First Order Logic Algorithm do not always terminate!
Problem: Find Algorithms that always terminate!
There might be no "naive" solutions!
First Order Logic Inference Algorithms (Tableaux Algorithm and Resolution) must be adapted for Description Logics
Tableaux Algorithm and Resolution show unsatisfiability of Theory (Knowledge Base)
Adaption of Entailment Problems to the Detection of Contradictions in the Knowledge Base, i.e. Proof of the Unsatisfiability to the Knowledge Base
