unicode_fol_kit.dl

The dl subpackage — the description logic ALC.

Concept constructors (import unicode_fol_kit.dl as dl):

dl.Top(), dl.Bottom(), dl.Atomic("Person"), dl.Not(C),
dl.And(C, D), dl.Or(C, D), dl.Exists("hasChild", C), dl.ForAll("hasChild", C)

Reasoning over a (general) TBox / ABox:

dl.concept_satisfiable(C, tbox)   # is C satisfiable w.r.t. the TBox?
dl.subsumes(C, D, tbox)           # does the TBox entail C ⊑ D?
dl.equivalent(C, D, tbox)         # C ≡ D?
dl.abox_consistent(abox, tbox)    # is the knowledge base consistent?

ALC is exactly multi-modal K; the reasoner is a tableau with TBox internalisation and subset blocking (see unicode_fol_kit.dl.tableau).

class unicode_fol_kit.dl.Concept

Bases: object

Base class for ALC concept expressions (see the module docstring).

to_unicode()

Render the concept with the standard DL glyphs (⊤ ⊥ ¬ ⊓ ⊔ ∃ ∀).

Return type:

str

class unicode_fol_kit.dl.Top

Bases: Concept

The universal concept ⊤ (every individual).

class unicode_fol_kit.dl.Bottom

Bases: Concept

The empty concept ⊥ (no individual).

class unicode_fol_kit.dl.Atomic(name)

Bases: Concept

A primitive concept name, e.g. Atomic("Person").

Parameters:

name (str)

name: str

class unicode_fol_kit.dl.Not(concept)

Bases: Concept

Concept complement ¬C.

Parameters:

concept (Concept)

concept: Concept

class unicode_fol_kit.dl.And(left, right)

Bases: Concept

Concept intersection C ⊓ D.

Parameters:

• left (Concept)

• right (Concept)

left: Concept

right: Concept

class unicode_fol_kit.dl.Or(left, right)

Bases: Concept

Concept union C ⊔ D.

Parameters:

• left (Concept)

• right (Concept)

left: Concept

right: Concept

class unicode_fol_kit.dl.Exists(role, concept)

Bases: Concept

Existential restriction ∃r.C — at least one role-successor is in concept.

Parameters:

• role (str)

• concept (Concept)

role: str

concept: Concept

class unicode_fol_kit.dl.ForAll(role, concept)

Bases: Concept

Value restriction ∀r.C — every role-successor is in concept.

Parameters:

• role (str)

• concept (Concept)

role: str

concept: Concept

unicode_fol_kit.dl.nnf(concept)

Return concept in negation normal form (negation only on atomic concepts).

Pushes ¬ inward with the De Morgan / modal dualities: ¬⊤ = ⊥, ¬⊥ = ⊤, ¬¬C = C, ¬(C⊓D) = ¬C⊔¬D, ¬(C⊔D) = ¬C⊓¬D, ¬∃r.C = ∀r.¬C, ¬∀r.C = ∃r.¬C.

Parameters:

concept (Concept)

Return type:

Concept

class unicode_fol_kit.dl.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.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.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.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.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.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.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

Modules

concepts	The description logic ALC: concept expressions, roles, and negation normal form.
tableau	An ALC tableau reasoner: concept satisfiability, subsumption, ABox consistency.