unicode_fol_kit.dl.concepts

The description logic ALC: concept expressions, roles, and negation normal form.

ALC (Attributive Language with Complements) is the smallest propositionally closed description logic and the notation underlying OWL. Its concepts describe sets of individuals and its roles binary relations between them:

• Top (⊤) — everything; Bottom (⊥) — nothing;

• Atomic("C") — a primitive concept name;

• Not(C) (¬C), And(C, D) (C ⊓ D), Or(C, D) (C ⊔ D);

• Exists("r", C) (∃r.C) — has an r-successor in C;

• ForAll("r", C) (∀r.C) — all r-successors are in C.

ALC is exactly the multi-modal logic K (a role r is a modality, ∃r its ◇ and ∀r its □), which is why it is decidable. nnf() rewrites a concept to negation normal form (negation only on atomic concepts), the shape the tableau in unicode_fol_kit.dl.tableau consumes.

The classes live in the dl namespace (import unicode_fol_kit.dl as dl); the names And / Or / Not are the concept constructors, distinct from the FOL AST’s connectives.

Functions

nnf(concept)

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

Classes

And(left, right)	Concept intersection C ⊓ D.
Atomic(name)	A primitive concept name, e.g. Atomic("Person").
Bottom()	The empty concept ⊥ (no individual).
Concept()	Base class for ALC concept expressions (see the module docstring).
Exists(role, concept)	Existential restriction ∃r.C — at least one role-successor is in concept.
ForAll(role, concept)	Value restriction ∀r.C — every role-successor is in concept.
Not(concept)	Concept complement ¬C.
Or(left, right)	Concept union C ⊔ D.
Top()	The universal concept ⊤ (every individual).

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

Bases: Concept

The universal concept ⊤ (every individual).

class unicode_fol_kit.dl.concepts.Bottom

Bases: Concept

The empty concept ⊥ (no individual).

class unicode_fol_kit.dl.concepts.Atomic(name)

Bases: Concept

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

Parameters:

name (str)

name: str

class unicode_fol_kit.dl.concepts.Not(concept)

Bases: Concept

Concept complement ¬C.

Parameters:

concept (Concept)

concept: Concept

class unicode_fol_kit.dl.concepts.And(left, right)

Bases: Concept

Concept intersection C ⊓ D.

Parameters:

• left (Concept)

• right (Concept)

left: Concept

right: Concept

class unicode_fol_kit.dl.concepts.Or(left, right)

Bases: Concept

Concept union C ⊔ D.

Parameters:

• left (Concept)

• right (Concept)

left: Concept

right: Concept

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