Change: Tableaux Algorithm (DL) with Blocking

created on March 10, 2013, 4:34 p.m. by Hevok & updated on March 10, 2013, 4:35 p.m. by Hevok

Blocking most times happens when one has an Existential Quantification. If one selects and Existential Quantification with an Individual a, in a Tableaux Path, this selection is blocked if there is already and Individual b if the following holds that all Classes to which a belongs are included in the Classes to which b belongs, then it is blocked. So one has two possibilities for Termination of this Algorithm. First thing, one is able to close the Tableaux, which means all Path are really closed, then the Knowledge Base is unsatisfiable and the original Assumption is True. Secondly, all non blocked selection from the Tableaux do not lead to an extension, then an Knowledge Base is satisfiable and the original assumption proves to be False.

If the Path is closed by blocking this means that the Knoweldge base is satisfiable and the original Assumption is not true.

  • The Selection of (∃R.C)(a) in the tableaux Path A is blocked, if there is already and Individual b with {C|C)(a)∈A}⊆{C|C(b)∈A}.
  • Two possibilities of Termination

    1. Closing the Tableaux.

    Knowledge Base is unsatisfiable.

    1. All non blocked Selections from the Tableaux do not lead to an Extension.

    Knowledge Base is satisfiable.

240px-Simplex-method-3-dimensions.png

Categories: Concept
Parent: Blocking

Comment: Corrected enumerated list.

See entry | Admin

Comment on This Data Unit