Created on March 10, 2013, 4:34 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.
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.
Comment on This Data Unit