Efficient TBox Reasoning with Value Restrictions using the $\mathcal{FL}_{o}$wer reasoner

To define the important notions of such an application domain as formal concepts, DLs state necessary and sufficient conditions for an individual to belong to a concept. These conditions can be Boolean combinations of atomic properties required for the individual (expressed by concept names) or properties that refer to relationships with other individuals and their properties (expressed as role restrictions). For example, the concept of a parent that has only daughters can be formalized by the concept description C: child.Human child.Female, which uses the concept names Female and Human and the role name child as well as the concept constructors conjunction (), existential restriction ( r.D), and value restriction ( r.D). Constraints on the interpretation of concept and role names can be formulated as general concept inclusions (GCIs). For example, the GCIs Human child.Human and child.Human Human say that humans have only human children, and they are the only ones that can have human children. DL systems provide their users with reasoning services that allow them to derive implicit knowledge from the explicitly represented one.