description logics

Description logics are a family of formal knowledge representation languages. Usually, their expressivity is between propositional logic and first order logic.

Description Logics


Below, we define the \(\mathcal{SROIQ}\) syntax.


RBox contains the roles axioms, roles are either the universal role or a role name \(r\) or its inverse \(r^{-}\).

The axioms are of the for \(r_{1} \circ r_{2} \circ \dots \circ r_{n} \sqsubseteq r\), si n > 1 it is called a transitivity statement.


Here, we list the possible concept expressions with \(C\) and \(D\) two concept expressions and \(r\) is a simple role:

  • top, bottom
  • nominal concepts, defined as finite set of individual name,
  • negation or complementary, if \(C\) is a concept expression, then \(\neg C\) is a concept expression too,
  • intersection, \(C \sqcap D\) is a concept expression,
  • union, \(C \sqcup D\) is a concept expression,
  • existential quantification, \(\exists r.C\) is a concept expression,
  • universal quantification, \(\forall r.C\) is a concept expression,
  • self restriction, if r is simple, \(\exists r.Self\) is a concept expression,
  • at-least restriction, for \(n\) a natural number, \(\geq n r.C\) is a concept expression,
  • at-most restriction, for \(n\) a natural number, \(\leq n r.C\) is a concept expression,

    Axioms are in a TBox are concept expressions inclusions, like \(C \sqsubseteq D\).


\(\mathcal{AL}\) is an abbreviation for attributive language. It allows the following concept descriptions:

  • atomic concepts, top and bottom
  • negation of atomic concept
  • intersection
  • universal quantification
  • limited existential quantification of the form \(\exists r. \top\)

    The AL language can be extended with union (\(\mathcal U\)), full existential quantification (\(\mathcal E\)), at-least and at-most restriction (\(\mathcal N\)) and negation (\(\mathcal C\)).


The letters S, R, O, I, F, N, Q

The letters:

  • \(\mathcal S\) denotes \(\mathcal{ALC}\), where we additionally allow transitivity statements,
  • \(\mathcal H\) in the name of a DL indicates that role hierarchy are supported,
  • \(\mathcal SR\) denotes \(\mathcal{ALC}\) with all kinds of RBox axioms as well as self concepts,
  • \(\mathcal O\) in the name of a DL indicates that nominal concepts are supported,
  • \(\mathcal I\) in the name of a DL indicates that inverse roles are supported,
  • \(\mathcal F\) in the name of a DL indicates that role functionally statements are supported (\(\perp \sqsubseteq \leq1 r.\top\)),
  • \(\mathcal N\) in the name of a DL indicates that unqualified at-least or at-most restrictions are supported, i.e. \(\leq n r.\top\) or \(\geq n r.\top\),
  • \(\mathcal Q\) in the name of a DL indicates that qualified number restrictions are supported.


The description logic EL

EL allows only concepts (no roles), which can be either the top concept, an atomic concept, the intersection of two concepts or the existential quantification of a concept (atomic or not). The TBox is a finite set of concept inclusions.



In DBLP:journals/logcom/Motik07, OWL-Full is represented as the most expressive of the Semantic Web ontology languages. Contrary to OWL-DL, OWL-Full does not impose the following restrictions:

  1. the sets of logical and metalogical symbols (e.g. rdf:type) are strictly separated,
  2. the sets of symbols used as concepts, roles and individuals are strictly separated,
  3. restrictions required to yield a decidable logic, such as the one on simple roles in number restrictions.

    Since 3. is not enforced in OWL-Full, OWL-Full is undecidable. The subset ALC-Full is undecidable if 1. and 2. are not enforced.



  • KAON2 is Java-based reasoner for query answering supporting SHIQ description logics,
  • FaCT++ is a free open-source C++-based reasoner
  • HermiT is a OWL reasoner based on hyper-tableau
  • Konclude is SROIQV(D) reasoner entirely supporting OWL

Knowledge base systems

  • RDFox is C++ in memory RDF triple store. It supports RDFS, datalog and OWL2 RL reasoning and SPARQL queries.


  • Protégé is a free, open-source ontology editor,
  • WebVOWL is a web visualizer for OWL file


  • Uli Sattler gives a talk about the description logics reasoners at KR 2021

This post accepts webmentions. Do you have the URL to your post?

Otherwise, send your comment on my service.

Or interact from the fediverse with your username:

fediverse logo Share on the Fediverse