unicode_fol_kit.dl.tableau

An ALC tableau reasoner: concept satisfiability, subsumption, ABox consistency.

Decides the core description-logic reasoning tasks for ALC with general TBoxes by the standard tableau algorithm. A tableau builds a tree of individuals, each carrying a label (a set of concepts it must satisfy), and applies completion rules:

• ⊓: x : C ⊓ D ⇒ add x : C and x : D (deterministic);

• ⊔: x : C ⊔ D ⇒ branch on x : C | x : D (nondeterministic);

• ∃: x : ∃r.C ⇒ create a fresh r-successor y with y : C;

• ∀: x : ∀r.C and x —r→ y ⇒ add y : C.

A clash is x : ⊥ or {x : A, x : ¬A}. A concept is satisfiable iff some branch saturates without a clash. General TBoxes C ⊑ D are internalised: the concept ¬C ⊔ D is forced on every individual. Termination with such axioms relies on subset blocking — a generated individual whose label is contained in that of an earlier individual is not expanded (its successors are reused), which is sound and complete for ALC (no inverse roles or number restrictions).

Public API: TBox, ABox, concept_satisfiable(), subsumes(), equivalent(), concept_unsatisfiable(), abox_consistent().

Functions

abox_consistent(abox[, tbox])	Return True iff the knowledge base (tbox, abox) is consistent (has a model).
concept_satisfiable(concept[, tbox])	Return True iff concept is satisfiable with respect to tbox.
concept_unsatisfiable(concept[, tbox])	Return True iff concept is unsatisfiable with respect to tbox.
equivalent(c, d[, tbox])	Return True iff tbox entails c ≡ d (mutual subsumption).
subsumes(sub, sup[, tbox])	Return True iff tbox entails sub ⊑ sup (every model puts sub in sup).

Classes

ABox([concept_assertions, role_assertions])	An ABox: concept assertions a : C and role assertions (a, b) : r.
TBox([inclusions])	A general TBox: concept inclusions C ⊑ D and equivalences C ≡ D.

class unicode_fol_kit.dl.tableau.TBox(inclusions=<factory>)

Bases: object

A general TBox: concept inclusions C ⊑ D and equivalences C ≡ D.

Parameters:

inclusions (List[Tuple[Concept, Concept]])

inclusions: List[Tuple[Concept, Concept]]

add(sub, sup)

Add a general concept inclusion sub ⊑ sup and return self (chainable).

Parameters:

• sub (Concept)

• sup (Concept)

Return type:

TBox

add_equivalence(c, d)

Add an equivalence c ≡ d (as the two inclusions c ⊑ d, d ⊑ c).

Parameters:

• c (Concept)

• d (Concept)

Return type:

TBox

internalized()

The concepts nnf(¬C ⊔ D) every individual must satisfy (one per GCI).

Return type:

List[Concept]

class unicode_fol_kit.dl.tableau.ABox(concept_assertions=<factory>, role_assertions=<factory>)

Bases: object

An ABox: concept assertions a : C and role assertions (a, b) : r.

Parameters:

• concept_assertions (List[Tuple[str, Concept]])

• role_assertions (List[Tuple[str, str, str]])

concept_assertions: List[Tuple[str, Concept]]

role_assertions: List[Tuple[str, str, str]]

assert_concept(individual, concept)

Add a concept assertion individual : concept (chainable).

Parameters:

• individual (str)

• concept (Concept)

Return type:

ABox

assert_role(a, b, role)

Add a role assertion (a, b) : role (chainable).

Parameters:

• a (str)

• b (str)

• role (str)

Return type:

ABox

unicode_fol_kit.dl.tableau.concept_satisfiable(concept, tbox=None)

Return True iff concept is satisfiable with respect to tbox.

Satisfiable means some model places an individual in the concept while obeying every TBox axiom. tbox=None is the empty TBox (pure concept satisfiability).

Parameters:

• concept (Concept)

• tbox (TBox | None)

Return type:

bool

unicode_fol_kit.dl.tableau.concept_unsatisfiable(concept, tbox=None)

Return True iff concept is unsatisfiable with respect to tbox.

Parameters:

• concept (Concept)

• tbox (TBox | None)

Return type:

bool

unicode_fol_kit.dl.tableau.subsumes(sub, sup, tbox=None)

Return True iff tbox entails sub ⊑ sup (every model puts sub in sup).

Decided by the standard reduction: sub ⊑ sup holds iff sub ⊓ ¬sup is unsatisfiable with respect to the TBox.

Parameters:

• sub (Concept)

• sup (Concept)

• tbox (TBox | None)

Return type:

bool

unicode_fol_kit.dl.tableau.equivalent(c, d, tbox=None)

Return True iff tbox entails c ≡ d (mutual subsumption).

Parameters:

• c (Concept)

• d (Concept)

• tbox (TBox | None)

Return type:

bool

unicode_fol_kit.dl.tableau.abox_consistent(abox, tbox=None)

Return True iff the knowledge base (tbox, abox) is consistent (has a model).

Parameters:

• abox (ABox)

• tbox (TBox | None)

Return type:

bool