Change: Decidability

created on March 9, 2013, 11:25 p.m. by Hevok & updated on March 9, 2013, 11:25 p.m. by Hevok

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.


Categories: Concept
Parent: Logic

Comment: Created entry.

See entry | Admin

Comment on This Data Unit