DL

In Description Logic (DL), the syntax of ALC includes a countable set of atomic concepts and a countable set of atomic roles.

In ALC, the top concept (⊤) and the bottom concept (⊥) are not considered as concepts.

The tableau calculus for ALC is a decision procedure for unsatisfiability.

In ALC, a concept is satisfiable if and only if it does not admit a model.

In the semantics of ALC, every atomic concept is mapped to a subset of the universe in an interpretation.

In an ABox, assertional axioms can include role assertions but not concept assertions.

The TBox in Description Logics is used to define terminologies through a set of definitions.

Subsumption in Description Logic is a partial order relation in the space of concepts.

The reasoning task of instance checking in ALC is reducible to satisfiability.

In the semantics of ALC, the negation of a concept is interpreted as the complement of the set of individuals.

The interpretation of a union of concepts corresponds to the union of their respective interpretations.

A TBox can contain both concept inclusions and concept equivalences.

Role assertions in an ABox relate individuals to other individuals via roles.

The consistency of an ABox can depend on the TBox it is associated with.

The interpretation of the existential quantification of a role includes all individuals that have a relationship through that role.

The interpretation of a concept in Description Logics is not necessarily a finite set.

Subsumption checking is undecidable for very expressive languages in Description Logics.

The concept of “closure” is relevant in the context of tableau algorithms for ALC.

An interpretation in Description Logics can be represented as a graph with nodes as individuals and edges as roles.

In ALC, every atomic role is interpreted as a binary relation over the universe of the interpretation.