Tableau algorithm for SHIN consistency checking

• The input syntax is KRSS - only part is implemented - see examples below.
• At present SHIN knowledge base consistency checking is implemented.
• The algorithm tries to find a model of given knowledge base. Candidate models are shown in the left tree. Two results of inference are possible:
  • either one of the models (tabs) is fully green - this means that this candidate model is valid for given concept, and the model is satisfiable. In this case the other models might be INCOMPLETE - the algorithm stops immediatelly after finding a valid model.
  • or in all models some nodes have red border - these nodes involve inconsistent assertions, and therefore we have not found a model.
• For visualization the JGraph + JGraphLayoutPro libraries have been used. The input syntax is KRSS.
• Some examples :

  • (instance I (and (some R A) (some R B) (not (some R (and A B)))))

  • (instance I (and (some R A) (some R B) (at-most 1 R) (not (some R (and A B)))))

  • (instance I (and (some R (and A B)) (not (and (some R A) (some R B)))))

  • (instance I (and (some P1 (all P2 (all P3 C11))) (some P1 (all P2 (all P3 C12))) (all P1 (and (some P2 (all P3 C21)) (some P2 (all P3 C22)) (all P2 (and (some P3 C31) (some P3 C32)))))))

  • (define-primitive-concept C (some R C))
    (instance I C)

  • (define-primitive-concept A (and (some R D) B))
    (define-primitive-concept B (at-least 1 R))
    (define-primitive-concept B F)
    (define-primitive-concept F (not E))
    (define-primitive-concept A (or  C D))
    (define-primitive-concept C (not E))
    (define-primitive-concept D F)
    (define-primitive-concept C (all R (not D)))
    (define-primitive-concept D (not B))
    (define-primitive-concept E (all R F))
    (instance I C)
    (instance I A)

  • (define-primitive-concept A (and (some R D) B))
    (define-primitive-concept B (at-least 1 R))
    (define-primitive-concept B F)
    (define-primitive-concept F (not E))
    (define-primitive-concept A (or  C D))
    (define-primitive-concept C (not E))
    (define-primitive-concept D F)
    (define-primitive-concept C (all R (not D)))
    (define-primitive-concept D (not B))
    (define-primitive-concept E (all R F))
    (instance I C)

• Reference - Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter Patel-Schneider, editors. The Description Logic Handbook, Theory, Implementation and Applications. Cambridge, 2003.