Reduction of Unsatisfiability

Created on March 9, 2013, 11:30 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.

For Inference one has to reduce the Problems for a Knowledge Base to unsatisfiability.

In the Class inconsistency one can do this if one checks whether the existing Knowledge Base combined with an instantiation of a Class is unsatisfiable. This can be accomplished with the Tableaux Algorithm or and adapted Resolution Algorithm.

Class inclusion is the Same way. Considering C is a Subclass of D. One can rewrite this with an negation, i.e. by combining an existing knowledge Base with and a Negation of the expression that computes to an Conjunction and one instantiates this, with an Individual a and one asks if this is unsatisfiable.

For Class Equivalence one has to proof Class Inclusion from one site and Class Inclusion from the other Site. So one has to double check the unsatisfiability.

If two Classes are Disjunct, the Intersection of two Classes must be empty, therefore one can ask whether the existing Knowledge Base combined with the Intersection of these two Classes, instantiated with a new individual, which should not exists, is unsatisfiable.

In Class Membership there one asks just whether the Knowledge Base combined with the negated Class Membership of a new Individual a where on checks Class Membership is unsatisfiable

For the Instance Generation /Retrieval Problem one has to check for all Individuals and check whether they are Member of the Class C or not. However, the question arises, is it really efficient or is it not efficient?

If one considers the principle Inference Problems, one has to transform them to an unsatisfiable problem to be able to apply the automatic Entailment algorithms adapt and applied to the Resolution Algorithm or the Tableaux Algorithm, which is based on unsatisfiability. As we have to proof the the Contradiction we have to transform these Problems and one can check these transformations.

  • Class (in)consistency C ≡ ⊥
    • if KB ⋃ {C(a)} unsatisfiable (a new)
  • Class Inclusion (Subsumption) C ⊑ D
    • if KB ⋃ {(C⊓¬D)(a)} unsatisfiable (a new)
  • Class Equivalency C ≡ D
    • if C ⊑ D and D ⊑ C
  • Class Disjointness C ⊓ D = ⊥
    • if KB ⋃ {(C⊓D)(a)} unsatisfiable (a new)
  • Class Membership C(a)
    • if ``KB ⋃ {¬C(a)} unsatisfiable
  • Instance Generation (Retrieval) "find all x with C(x)"
    • Check class membership for all individuals
    • but: efficiency?
miku_is_unsatisfied.jpg

Tags: transformation, logic, inference
Categories: Concept
Parent: Logic

Update entry (Admin) | See changes

Comment on This Data Unit