Change - DInferencidae Probilityems

Created on March 9, 2013, 11:19 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. ¶
¶
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 BaseInference and Entailment for Description Logics can be applied on specific problems that one wants to answer with the help of a given Knowledge Base. In general the Problems of Inference are the following. ¶
First of all one is interested whether a Knowledge Base as a whole is consistent or not he other hand if is possible that one can entail the bottom element from a Knowledge base, the it is not consistent. ¶
¶
What can be done for the entire Knowledge Base can also be done for single Class. One can ask whether a Class definition is consistent or must be Class be empty, because the definition is wrong. ¶
¶
On the other hand one can also ask whether a Class inclusion, a Subsumption, i.e. C is part of D. Does is hold or does it not hold? ¶
¶
Also one can also ask about Class equivalency, is C equal to D, so are two Classes really the same? ¶
¶
If one compares two Classes it is also possible that these two Classes disjunctive which means that no Individual is at the same time in Class C and in Class D. One can ask for this, whether two Class are Conjunctive. ¶
¶
It might also be interesting to ask for Class Membership, i.e. is an Individual a contained in class C? ¶
¶
Another thing which one might ask is Instance generation which is a retrieval Problem, i.e. find all x with the Condition C of x which means find all x that are within the Class C. ¶
¶
* Global (In)Consistency of the Knowledge Base ¶
- Does the Knowledge Base make sense? KB ⊨ ⊥? ¶
* Class(in)consistency ¶
- Must Class C be empty? C ≡ ⊥? ¶
* Class Inclusion (Subsumption) ¶
- Structuring the knowledge Base ¶
* Class Equivalency ¶
- Are two Classes the same? ¶
* Class Disjointness ¶
- Are two Classes disjunctive? ¶
* Class Membership C(a)? ¶
- Is individual a contained in Class C? ¶
* Instance Generation (Retrieval)* "find all x with C(x)" ¶
- Find all (known!) Individuals of Class C