We propose an extension of Description Logics (DLs) with generic concepts and conditional axioms. Inspired by object-oriented languages, generic concepts allow a compact definition of concepts with similar structures. For example, one can define a generic concept Owner[X] to describe objects that own another object from X, and later use a specific replacement of the parameter X, such as Owner[Pet] representing pet owners. Conditional axioms can be used to set bounds on the values that replace the generic parameters. For example, we could restrict replacements of X in a concept Feeder[X] to only subconcepts of Pet. As the set of possible parameter replacements can be infinite and even uncountable, the generic extensions are, in general, undecidable. To identify decidable generic DLs, we focus on the case of terminologies, requiring that variables are only used in definitions of generic concepts. We formulate syntactic restrictions that allow reducing generic to classical entailment and further conditions that ensure decidability.
Many large Description Logics (DLs) ontologies exhibit regularities in their syntactic structure [
Generic axioms can be interpreted in two ways: using the schema semantics and using the secondorder semantics [13]. Under the schema semantics, the axiom Owner[ ] ≡ ∃ owns. is regarded literally as an abbreviation of (countably-many) axioms Owner[] ≡ ∃ owns. obtained by replacing the concept variable with all possible concepts from the language. Under the second-order semantics, concept variables can be replaced with arbitrary subsets of the interpretation domain. Second-order semantics is, generally, stronger than the schema semantics because not every subset of a domain is an interpretation of some concept of the language. However, entailment under the schema semantics can be computed using standard DL algorithms by treating instances of parametrized concepts such as Owner[Pet] and Owner[Car] as distinct atomic concepts. Schema entailment, however, may depend on the language in which the replacement concepts are constructed: replacing with ℰ ℒ concepts may result in fewer entailments than replacing with ℒ concepts (and fewer than for the second-order entailment). Therefore, a central question for generic DLs is, when both semantics result in the same entailments.
The previous work on generic DLs [13] shows that it is possible to ensure that second-order entailment coincides with the schema entailment by limiting the base language to DL ℰ ℒ and applying further syntactic restrictions. In this paper, we use a diferent approach: Instead of restricting the type of concept constructors that can be used in ontologies, we restrict the shape of axioms. Specifically, we allow definitions of (generic) atomic concepts of form [1, . . . , ] ≡ where the left-hand side is a parametrized concept and the right-hand side is an arbitrary (ℛℐ) concept containing only the variables (1 ≤ ≤ ) present on the left. A terminology is a set of such concept definitions in which every concept is defined at most once. We can also allow partial concept definitions of the form [1, . . . , ] ⊑ , also when the partially defined atomic concept may appear in several such partial definitions, because they can be rewritten to concept definitions using concept conjunction and fresh atomic concepts. We also allow the ontology to contain any number of ground axioms, i.e., axioms that do not contain concept variables.
Sometimes, it is useful to further restrict (partial) definitions by limiting the scope of parameters for which they can be used. For this purpose, we introduce a new type of axiom called conditional axiom. Similarly to bounds in generic programming [12], conditional axioms allow for restricting the concepts/domain-subsets that are considered for concept variables. A conditional axiom consists of a range of conditions and a target axiom: { 1, . . . , } ⇒ , the conditions, as well as the target axiom, are classical axioms (potentially using generic concepts). For example, this allows us to specify diferent kinds of contents: ⊑ ⇒ [] ⊑ , ⊑ ⇒ [] ⊑ , ⊑ ⇒ [] ⊑ ℎ. If a parameterized concept is applied to an argument that is not satisfied by the conditions, we consider it to be undefined, and it can be interpreted arbitrarily, which aligns with the idea of partial definitions. The terminological part of ontologies that we specify can also be cyclic. For example, our DL extension is able to capture recursive data definitions such as a node of a tree-structure: Node[] ≡ ∀ hasSuccessor.Node[] ⊓ ∃hasValue.
In this paper, we present the following results. First, we show that reasoning under classical ontologies extended with (only) conditional axioms can be reduced to reasoning with classical ontologies allowing for negated axioms (Section 4). Second, using the conditional axioms, we show that entailment for ground generic ontologies can be reduced to entailment for classical ontologies (with conditional axioms) (Section 5). Third, we show that we can reduce reasoning with a non-ground generic terminology to reasoning with a ground generic ontology using a fixpoint approach; this approach allows us to extend a model of the ground part of a generic terminology to a model of the whole ontology (Section 6). In Section 7, we explain how the semantic restrictions from Section 6 can be achieved syntactically in practice. We start out with a discussion of related work (Section 2), followed by the formal introduction of the generic extension using conditional axioms (Section 3), and conclude with a discussion of our results (Section 8).
Due to limited space, we provide most proofs and examples in the appendix.
As mentioned in the introduction, our work is based on the existing generic extension of description logics [13]. We difer from that work in the way we restrict the usage of generic features to keep decidability. Instead of restricting the generic DL to a fragment of the extension of ℰ ℒ, we work with the extension of DLs up to ℛℐ, but require that axioms with variables are part of a terminology where each parameterized concept is defined at most once (multiple partial definitions are also allowed). Additionally, we introduce a new feature of the generic extension in this paper, namely, conditional axioms that allow us to restrict the range of concept variables using classical axioms.
Apart from generic extensions, our approach is related to several other areas. Ontology parts
of similar syntactic structure are primarily studied in the field of Ontology Design Patterns ( ODPs)
[3, 4, 5, 6, 7, 8, 9]. Similar to our reduction of second-order to classical reasoning, this method employs
variables to create axiom templates for deriving standard axioms tailored to particular applications.
The key distinction from our approach is that ODPs lack true generic concepts like Owner[] and do
not possess model-theoretic semantics. Rather, ODPs are generally a preliminary stage, substituting
variables with concepts from predetermined sets of candidates to form a classical ontology that can
subsequently be used in the standard way. There are also works in this area that are primarily concerned
with finding repeating structures in ontologies (usually with the goal of testing and defining new ODPs)
[
A related but diferent concept are the Generators introduced by Kindermann et al. [ 10]. Those are a kind of rule language on top of DLs, consisting of rules called generators that have axiom templates as conditions and targets. If a certain replacement of variables in the conditions results in an axiom that is entailed by the ontology, then the target is added as an axiom to the ontology for the same variable replacement. This is somewhat similar to our conditional axioms, with the most important diference being that usage of these generators requires the (manual) specification of a language of replacement concepts, while in our case, the second-order semantics considers arbitrary subsets of the domain as replacements of the concept variables.
Additionally, in the broader context of DL research, the idea of making axioms depend on other
axioms in the DL itself, like we do with conditional axioms, is also not completely new. One example
are so-called context description logics [
We start by formally defining the syntax of generic DLs with parameterized concepts, concept variables, and conditional axioms.
Definition 1 (Syntax, extended from [13]). The syntax of generic DLs consists of disjoint and countably infinite sets of concept names, each with an assigned arity ar() ∈ N ( ∈ ), of role names, and of concept variables. Given a base DL L that is a fragment of ℛℐ, we define by L its corresponding generic extension, adding parameterized (atomic) concepts, concept variables, and conditional axioms. Specifically, the set of L -concepts is the smallest set containing concept variables ∈ , concept terms [1, . . . , ], where ∈ , = ar() and are L -concepts (1 ≤ ≤ ), and which is closed under the concept constructors of L. The set of L -axioms is the smallest set containing all axioms built from L -concepts using the axiom constructors of L, as well as axioms of the form Γ ⇒ ( conditional axioms), where is a non-conditional L axiom and Γ is a set of such axioms. An L -ontology is a (possibly infinite) set of L -axioms.
For a conditional axiom = (Γ ⇒ ), we call all elements ∈ Γ conditions of and the target
of . All axioms that are not conditional axioms, i.e., Γ is empty, we call unit axioms. Note that all
conditions and the target can only be unit axioms; conditional axioms can not be nested.1 We introduce
a range of special notations to facilitate the discussion about L concepts and axioms.
Definition 2 (Adapted from [13]). Let the expression be either a L -concept, a L -axiom, or a
L -ontology. We denote by sub() (all) subconcepts of , i.e., substrings of the expression that are valid
concepts. For L -concepts and L -axioms (that are not using ⇒), we split sub() into sub+() and
sub− () the set of concepts that occur positively, respectively negatively, in , sub() = sub+() ∪
sub− (). For simple DLs occurring positively (negatively) simply corresponds to occurring on the right
1If conditional axioms were allowed to be nested, we would be able to express all boolean combinations over axioms.
side of the axiom under an even (odd) number of nested negations or on the left side under an odd (even)
number of nested negations, for more expressive DLs this can be more dificult, see e.g., [
A (concept variable) substitution is a partial mapping = [1/1, . . . , /] that assigns concepts to concept variables (1 ≤ ≤ ). We denote by () the result of applying the substitution to , defined in the usual way.
In the remainder of the paper, we diferentiate between diferent versions of a DL as follows: If concepts, axioms, and ontologies include concept terms, conditional axioms, and concept variables, we call them generic. If this is not the case, i.e., the DL is not extended by us, we call these classical.
As described in Section 1, we adapt the existing second-order semantics for generic extensions [13] for usage with conditional axioms:
is a pair ℐ = (∆ ℐ , · ℐ ), where ∆ ℐ is a nonempty set called the domain of ℐ and · ℐ is an interpretation function, which assigns to every ∈ with arity = ar() a function ℐ : (2Δℐ ) → 2Δℐ and to every ∈ a relation ℐ ⊆ ∆ ℐ × ∆ ℐ . A valuation for ℐ (also called a variable assignment) is a mapping that assigns to every variable ∈ a subset () ⊆ ∆ ℐ .
The interpretation of L -concepts ℐ, ⊆ ∆ ℐ is recursively defined by ℐ, = () for ∈ , [1, . . . , ]ℐ, = ℐ (1ℐ, , . . . , ℐ, ), and is extended to other L -concepts in the usual way. Satisfaction of unit axioms ℐ |=2 under ℐ and is determined from the interpretation of L -concepts in in the standard way. For example, ℐ |=2 ⊑ if ℐ, ⊆ ℐ, . The interpretation of conditional axioms follows naturally, i.e., ℐ |=2 Γ ⇒ , if ∃ ∈ Γ : ℐ ̸|=2 or ℐ |=2 . We write ℐ |=2 if ℐ |=2 for every valuation . Finally, for an ontology , we write ℐ |=2 if ℐ |=2 for every ∈ , and we write |=2 if ℐ |=2 implies ℐ |=2 .
We add a few remarks about this definition: First, for a classical ontology every second-order model is a classical model and vice versa as the second-order interpretation only difers from a classical interpretation in its treatment of atomic concepts (which we call parameterized concepts in the generic DL) as functions, which is not relevant if we only have atomic/parameterized concepts with zero arity as in the case of classical ontologies. Second, notice that for our conditional axioms, the same is considered for the conditions, as for the target, i.e., the ∀ quantification is outside the implication. This is important as we want conditions to restrict the choice of subsets of the domain that are considered for the variables in the target axiom. For example, all usages of in { ⊑ Pet} ⇒ Keeper[] ≡ ∃ owns. ⊓ ∃feeds. , must be the same, and describe some kind of pet. Finally, we can easily reduce the entailment of a ground axiom Γ ⇒ , i.e., |= Γ ⇒ , to the unsatisfiability of extended with Γ and the conditional axiom { } ⇒ ⊤ ⊑ ⊥: Clearly, |= Γ ⇒ if ∪ Γ |= and if ∪ {{ } ⇒ ⊤ ⊑ ⊥} is unsatisfiable, then ℐ |= holds for every model ℐ of , therefore |= Γ ⇒ if ∪ Γ ∪ {{ } ⇒ ⊤ ⊑ ⊥} is unsatisfiable.
We start our analysis by considering the new feature introduced in this paper, i.e., conditional axioms, on their own. That is, we consider the extension of classical DLs (only) with conditional axioms (not yet concept terms or concept variables). For example, we allow axioms such as { ⊑ , ⊑ } ⇒ ∃. ⊑ ⊤.
This extension can be nondeterministically reduced to reasoning with negated axioms by choosing for each conditional axiom either the target axiom or the negation of some condition axiom. Then the satisfiability of our ontology with conditions coincides with the satisfiability of (at least) one of these constructed ontologies.
The reduction described in Theorem 1 can be used for DLs, which can express negation of the axioms appearing as conditions. For example, negations of concept inclusion axioms ⊑ can be expressed as {(), (¬)()} with a fresh individual. Of course, for a less expressive DL like ℰ ℒ, this raises the complexity of reasoning, as efectively we are using ℒ reasoning.
The approach described in the previous section allows us to remove conditional axioms from ontologies to be able to use classical interpretations instead of second-order ones. With this result, only two features still make it dificult to consider a generic ontology under classical interpretations. The first are variables, the second are concept terms. We can leave variables aside for now by considering only ground generic ontologies. To deal with concept terms, a naive way to interpret them under classical interpretations is to simply consider them as new atomic concept names.2 Unfortunately, this has the side efect that we do not account for equivalent axioms anymore, i.e., using classical interpretations in this way for an ontology such as { ≡ } we do not get [] ≡ [] as a consequence because [] and [] are two independent atomic concepts. On the other hand, clearly, for second-order semantics, we get [] ≡ [] as the function applied to the same set = ℐ = ℐ twice, gives the same result. To still be able to reduce second-order entailment to classical entailment using this approach, we transform the given ontology using a closure that moves this treatment of equal concepts from the semantics to explicit (conditional) axioms in the ontology:
=1 ≡ ⇒ [1, . . . , ] ≡ [1, . . . , ] where = ar() and , , L -concepts (1 ≤ ≤ ). The congruence closure of a ground ontology is the extension of with all congruence axioms for which [1, . . . , ] ∈ sub() and [1, . . . , ] ∈ sub().
Clearly, all congruence axioms are tautologies under the second-order semantics: Lemma 2. Let be a congruence axiom and ℐ a second-order interpretation. Then ℐ |=2 . Lemma 3. Let be a ground ontology and ′ the congruence closure of (see Definition 4). Then is satisfiable under second-order semantics if ′ is (classically) satisfiable.
of by setting [1, . . . , ] = ℐ (1ℐ , . . . , ℐ ). But then this new classical interpretation is still a model of and by Lemma 2 also a model of ′. (⇐) Likewise we can construct a second-order interpretation ℐ from a classical model of ′ by setting ℐ (1, . . . , ) = [1, . . . , ] if there are such s that = . If this is not the case we set ℐ (1, . . . , ) = ∅ as the default. Using the presence of the equivalence axioms, we can show that the choice of 1, . . . , is unambiguous.
Theorem 4. Second-order satisfiability of ground ontologies with conditional axioms can be reduced in polynomial time to satisfiability of ground ontologies with conditional axioms under classical semantics. 2This was done in the existing work on generic extensions, leading to syntactic restrictions [13].
Following the results regarding ground ontologies, in this section, we extend our results to the nonground case. The goal of this section is to reduce the (second-order) satisfiability of generic non-ground ontologies to the (second-order) satisfiability of generic ground ontologies. With the results from the previous sections, this gives us the ability to reduce reasoning with generic ontologies to classical reasoning (with negated axioms).
Our approach works under the assumption that a given generic ontology consists of two parts: a
ground part containing arbitrary ground axioms and a terminological part consisting of generic concept
definitions. Our main result shows that, under certain semantic conditions, an arbitrary model of
the ground part can be extended to a model of the terminological part by using a fixpoint operator
reminiscent of defining the least fixpoint semantics for (cyclic) ℰ ℒ terminologies [
For a given generic terminology, we call parameterized concepts that occur as the defined concept of a complete concept definition, completely defined concepts , denoted as def, and parameterized concepts that occur as the defined concept of a partial concept definition, partially defined concepts , denoted as part. All other parameterized concepts occurring in the terminology are called primitive concepts, denoted prim. It should be noted that we permit cyclic dependencies among the defined concepts. We do not consider an axiom as a proper complete concept definition if a variable occurs in the conditional axiom, but not as an argument of the defined concept. In this case, the definition would not be unambiguous, for example, [] ≡ ⊓ ∃. does not clearly define how [] should be interpreted. This problem does not occur for partially defined concepts, as in cases where a complete definition would be ambiguous, the option that interprets the parameterized concept as the smallest set can be chosen. See Example 1 for a number of examples of concept definitions.
As said above, we want to take a model of the ground part of an ontology and extend it to a model of the whole ontology (including the non-ground but terminological part). This means that given a model of the non-ground part ℐ, we can only change the interpretation of parameterized concepts for arguments that do not occur in the ground part, e.g., if [] is a concept in the ground ontology, we may not change the interpretation of ℐ ( ) for the argument = ℐ in order to ensure that our resulting interpretation still is a model. What we can change is the interpretation for “unknown” s. We formalize these allowed changes in the following definition.
Definition 6 (Terminological Expansions). Let be a ground generic ontology, a generic terminology, and ℐ a model of , i.e., ℐ |= . We call a set ⊆ ∆ ℐ known if there is a ∈ sub() such that ℐ = , otherwise it is unknown. A subset of (∆ ℐ ) is unknown if at least one member is unknown. Then a terminological expansion of ℐ is an interpretation = (∆ , · ), such that ∆ = ∆ ℐ , ∀ ∈ : = ℐ , ∀ ∈ sub() : = ℐ , for ∈ part and 1, . . . , ⊆ ∆ ℐ unknown, (1, . . . , ) = ∅, and ∀ ∈ prim : = ℐ . By Tx, (ℐ) we denote the set of all terminological expansions of ℐ. We omit and if they are irrelevant or clear from the context.
We additionally define the following ordering on Tx(ℐ): If 1, 2 ∈ Tx(ℐ), then 1 ⪯ ℐ 2 if ∀ ∈ def, ∀1, . . . , ⊆ ∆ ℐ : (1, . . . , )1 ⊆ (1, . . . , )2 .
are applied to unknown arguments, i.e., to subsets of the domain that are not “represented” by any concept that occurs in . This makes sure that for all concepts in , and ℐ coincide, i.e., |=2 .
We choose to interpret partially defined concepts as the empty set in the expansions. The advantage of this is that for partially defined concepts and unknown arguments, we immediately know that their definition is entailed by every ∈ Tx, (ℐ).
Definition 7.
An L -ontology is said to be admissible if = ∪ , where: 1. is a ground ontology, 2. is a (generic) terminology, 3. If [1, . . . , ] is defined by some ∈ then for every substitution such that ([1, . . . , ]) ∈ sub() it holds that |=2 ( ), 4. If is the description of some completely defined concept in , ℐ a model of and 1 ⪯ ℐ 2, then 1, ⊆ 2, for every valuation .
The notion of an admissible ontology ensures that an extension of a model of the ground part to a model of the terminological part is always possible. Condition 3 prevents a clash of the knowledge of the ground and the terminological parts, e.g., having an axiom ⊤ ⊑ [] in and an axiom [] ≡ ⊥ in violates this condition. Furthermore, Condition 3 ensures that for known arguments, definitions in are entailed by every ∈ Tx, (ℐ). This means we do only need to choose a ∈ Tx, (ℐ) that also entails complete definitions for unknown arguments to get a model of . To find this , we use an approach that (starting from ℐ) changes the interpretation of completely defined concepts step-by-step to get closer to their definition, until a fixpoint is reached.
For such a fixpoint to exist, we need to make sure that the interpretation only increases from step
to step. Because we allow defined concepts in the descriptions in , this can only be ensured if
descriptions are always upward monotone in all fully defined concept terms. For example, if we had
[] ≡ ¬ [], this would not hold, as if we assume that [] increases with every step of our
expansion, then [] would at the same time decrease. Indeed, if this monotonicity were not required,
we would be able to express General Concept Inclusions (GCIs) in our terminology. The reason for
this is similar to absorption [
Definition 8 (One Step Expansion). Let = ∪ be an admissible ontology according to Definition 7 and ℐ a model of . The one-step expansion is a function 1Exp,ℐ : Tx, (ℐ) → Tx, (ℐ) such that 1Exp,ℐ ( ) is the interpretation ′ ∈ Tx, (ℐ) defined by changing the interpretation of completely defined concepts in the following way: Let ∈ def, 1, . . . , ⊆ ∆ ℐ unknown, if is defined by Γ ⇒ [1, . . . , ] ≡ ∈ then for = {1/1, . . . , /}: ′ (1, . . . , ) = ,
Intuitively, the one-step expansion 1Exp( ) is the result of updating the interpretation of completely defined concepts (when applied to unknown arguments) by using their description. Note that the conditions of Definition 5 ensure that one-step expansion of is well-defined. In particular, the definition is unambiguous because every parameterized concept is completely defined in at most once, and all concept variables appearing in this definition must be parameters of this concept. In this procedure, we do not take the conditions Γ into consideration, because if we make sure that in the extended model the definition [1, . . . , ] ≡ holds for every choice of , then it also holds in the cases where Γ is also entailed. Disregarding Γ can also not lead to contradictions: A contradiction with another axiom in is not possible, because every parameterized concept is only completely defined once (regardless if conditions are present or not); And a contradiction with is not possible because of we only change the interpretation for unknown arguments.
We are now ready to show the final result of this section. We use here that the one-step expansion we defined is a monotone function on the set of terminological expansions, giving us the guaranteed existence of a fixpoint. This fixpoint is our new model of the whole ontology .
Proof sketch. Given a model ℐ = (∆ ℐ , · ℐ ) of , we show that the fixpoint of 1Exp,ℐ exists and is a model of . To show this, we use our Requirement 4 of Definition 7, which gives us the monotonic behavior of descriptions. From this, the monotonic behavior of the one-step expansion follows naturally.
of the one-step expansion. This fixpoint is (still) a model of the ground part of the ontology, but also of the terminological part. This follows because, as it is a fixpoint, the one-step expansion does not change the interpretation of defined concepts anymore; therefore, those defined concepts already correspond to their description, and the definitions in are modeled.
In the previous section, we have shown that the satisfiability of a generic ontology with an arbitrary ground part and a terminological non-ground part can be reduced to the satisfiability of the ground part only. The requirement for this result is, that the given ontology is admissible, i.e., fulfills certain restrictions: First, for a defined concept, the definition must already be entailed for known arguments by the ground part (Case 3 of Definition 7), second the descriptions of completely defined concepts need to be (upward) monotone in the contained completely defined concepts, i.e., increase if the interpretation of subterms increases (Case 4 of Definition 7). In this section, we discuss how these restrictions can be achieved in practice.
Definition 9 (Ground Expansion). Given a generic ontology , consisting of a ground part and a generic terminology , i.e., = ∪ , we define the ground expansion Exp() as the set of axioms achieved in the following way: All axioms in are in Exp(). Then we repeatedly check if for [1, . . . , ] ∈ sub(Exp()) such that is defined by in , we have Exp() |=2 ( ) for = {1/1, . . . , /}. If this is not the case, we add ( ) to Exp(). We repeat this until no new axioms are added to Exp().
This procedure does not terminate in every case. To achieve termination, it is important that there are no nested concept terms in . If this were the case, e.g., we would have 1[2[]] ∈ sub( ), then any replacement of with a concept from [. . . , , . . . ] ∈ sub(Exp()) results in a new concept 1[2[]] ∈ sub(Exp()), which again results in a new concept 1[2[2[]]] ∈ sub(Exp()) and so on. This would result in an infinite Exp(). If we do not have such nested concept terms, calculating the expansion of takes at most exponential time. This is because, in the worst case, we have to ground every terminological axiom with every set of concepts occurring as arguments of concept terms in .
instances of axioms in . Furthermore, it is easy to see that now ′ = Exp() ∪ fulfills Case 3 of Definition 7, therefore (assuming that Case 4 of Definition 7 also holds) we can check the satisfiability of Exp() to determine if is satisfiable by Theorem 5.
We now consider how to achieve the monotonicity of concept descriptions (i.e., Case 4 of Definition 7).
A simple syntactic condition that is suficient to achieve this monotonicity is to require that concept
terms using a completely defined concept may only occur positively in a concept description. It is
well known that positive polarity of subterms results in the concept being upward monotone in the
subterm (see e.g., [
Taking these remarks together with our earlier results, we obtain the following reduction as a consequence of Theorems 1, 4, and 5: Corollary 6. Given a generic ontology satisfying the following conditions: (1) Axioms are either ground or concept definitions; (2) there are no nested concept terms in these definitions; and (3) non-ground concept terms using completely defined concepts only occur positively in descriptions. The satisfiability of under second-order semantics can be reduced in exponential time to the satisfiability of classical ontologies with negated axioms.
Generic DLs were introduced to eficiently handle collections of similar axioms in ontologies, ofering advantages akin to those of generic classes in programming: A parameterized concept’s definition can be applied in various contexts, minimizing the necessity for duplicating and altering intricate concept structures. This method supports modular ontology construction and aids in preventing mistakes that may occur during axiom refactoring. Unfortunately, existing generic extensions [13] were limited to fragments of the extension of ℰ ℒ.
In this paper, we lift this restriction, showing the decidability of generic extensions of expressive
parameterized concepts, while they can be used freely when ground. This is a reasonable restriction as this captures the initial idea of generic concepts, namely being a way to combine the definition of many similar concepts into one place. It also corresponds to the historic development of DLs, which also started with terminologies.
We also introduce a new feature of generic extensions, namely, conditional axioms. These allow us to formulate conditions under which an axiom should hold, while in interpretations where these conditions do not hold, the axiom can be ignored. Conditional axioms are a natural addition to generic DLs, akin to bounds in generic programming. They can be used as a check on variable replacements in concept terms, allowing to select one (or more) of potentially many partial definitions given for a parameterized concept in an ontology. Furthermore, conditional axioms are also an advantage for complete definitions, for example, we can formulate that the definition of Keeper[] “makes sense” only when describes some set of pets, i.e., { ⊑ Pet} ⇒ Keeper[] ≡ ∃ owns. ⊓ ∃feeds.. This prevents modeling errors, where Keeper[· ] is used with some wrong argument, such as Keeper[Car].
Planned future work involves an implementation of the approach presented here, as well as studies to analyze the potential of existing ontologies to benefit from generic extensions, i.e., what reduction of inherent complexity is possible, as well as a tool for an automatic translation of existing ontologies to the generic extension.
In summary, the findings in this paper demonstrate that it is possible to get generic extensions of expressive description logics that are still decidable, provided certain reasonable restrictions are applied. Additionally, the introduction of conditional axioms allows to use generic concepts in a more targeted way, by restricting the replacement of parameters. This is a valuable addition to the area of generic description logics, as well as to the broader research area that deals with exploiting syntactic regularities in ontologies.
During the preparation of this work, the authors used Writefull, Grammarly and GPT-4/5 in order to paraphrase content and do grammar and spelling checking. After using these tools, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. [2] E. Mikroyannidi, N. A. A. Manaf, L. Iannone, R. Stevens, Analysing syntactic regularities in ontologies, in: P. Klinov, M. Horridge (Eds.), Proceedings of OWL: Experiences and Directions Workshop 2012, Heraklion, Crete, Greece, May 27-28, 2012, volume 849 of CEUR Workshop Proceedings, CEUR-WS.org, 2012. URL: https://ceur-ws.org/Vol-849/paper_11.pdf. [3] A. Gangemi, V. Presutti, Ontology design patterns, in: S. Staab, R. Studer (Eds.), Handbook on Ontologies, Springer Berlin Heidelberg, 2009, pp. 221–243. URL: http://link.springer.com/10.1007/ 978-3-540-92673-3_10. doi:10.1007/978-3-540-92673-3_10. [4] Y. He, J. Zheng, Y. Lin, Ontorat: Automatic generation and editing of ontology terms, in: F. M.
Couto, J. Hastings (Eds.), Proceedings of the International Conference on Biomedical Ontology, ICBO 2015, Lisbon, Portugal, July 27-30, 2015, volume 1515 of CEUR Workshop Proceedings, CEURWS.org, 2015. URL: https://ceur-ws.org/Vol-1515/demo2.pdf. [5] M. G. Skjaeveland, D. P. Lupp, L. H. Karlsen, H. Forssell, Practical ontology pattern instantiation, discovery, and maintenance with reasonable ontology templates, in: D. Vrandecic, K. Bontcheva, M. C. Suárez-Figueroa, V. Presutti, I. Celino, M. Sabou, L. Kafee, E. Simperl (Eds.), The Semantic Web - ISWC 2018 - 17th International Semantic Web Conference, Monterey, CA, USA, October 8-12, 2018, Proceedings, Part I, volume 11136 of Lecture Notes in Computer Science, Springer, 2018, pp. 477–494.
URL: https://doi.org/10.1007/978-3-030-00671-6_28. doi:10.1007/978-3-030-00671-6\_28. [6] B. Krieg-Brückner, T. Mossakowski, F. Neuhaus, Generic ontology design patterns at work, in: A. Barton, S. Seppälä, D. Porello (Eds.), Proceedings of the Joint Ontology Workshops 2019 Episode V: The Styrian Autumn of Ontology, Graz, Austria, September 23-25, 2019, volume 2518 of CEUR Workshop Proceedings, CEUR-WS.org, 2019. URL: https://ceur-ws.org/Vol-2518/paper-BOG2.pdf. [7] M. G. Skjaeveland, H. Forssell, J. W. Klüwer, D. P. Lupp, E. Thorstensen, A. Waaler, Reasonable ontology templates: APIs for OWL, in: N. Nikitina, D. Song, A. Fokoue, P. Haase (Eds.), Proceedings of the ISWC 2017 Posters & Demonstrations and Industry Tracks co-located with 16th International Semantic Web Conference (ISWC 2017), Vienna, Austria, October 23rd - to - 25th, 2017, volume 1963 of CEUR Workshop Proceedings, CEUR-WS.org, 2017. URL: https://ceur-ws.org/Vol-1963/ paper597.pdf. [8] A. Borgida, J. Horkof, J. Mylopoulos, R. Rosati, Experiences in mapping the business intelligence model to description logics, and the case for parametric concepts, in: Y. Kazakov, D. Lembo, F. Wolter (Eds.), Proceedings of the 2012 International Workshop on Description Logics, DL-2012, Rome, Italy, June 7-10, 2012, volume 846 of CEUR Workshop Proceedings, CEUR-WS.org, 2012. URL: https://ceur-ws.org/Vol-846/paper_48.pdf. [9] C. Kindermann, B. Parsia, U. Sattler, Comparing approaches for capturing repetitive structures in ontology design patterns, in: K. Janowicz, A. A. Krisnadhi, M. Poveda-Villalón, K. Hammar, C. Shimizu (Eds.), Proceedings of the 10th Workshop on Ontology Design and Patterns (WOP 2019) co-located with 18th International Semantic Web Conference (ISWC 2019), Auckland, New Zealand, October 27, 2019, volume 2459 of CEUR Workshop Proceedings, CEUR-WS.org, 2019, pp. 17–31. URL: https://ceur-ws.org/Vol-2459/paper2.pdf. [10] C. Kindermann, D. P. Lupp, U. Sattler, E. Thorstensen, Generating ontologies from templates: A rule-based approach for capturing regularity, in: M. Ortiz, T. Schneider (Eds.), Proceedings of the 31st International Workshop on Description Logics co-located with 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), Tempe, Arizona, US, October 27th - to - 29th, 2018, volume 2211 of CEUR Workshop Proceedings, CEUR-WS.org, 2018. URL: https://ceur-ws.org/Vol-2211/paper-22.pdf. [11] C. Kindermann, A.-M. George, B. Parsia, U. Sattler, Minimal macro-based rewritings of formal languages: Theory and applications in ontology engineering (and beyond), in: Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, 2024, pp. 10581–10588. URL: https: //ojs.aaai.org/index.php/AAAI/article/view/28928, issue: 9. [12] R. Garcia, J. Jarvi, A. Lumsdaine, J. G. Siek, J. Willcock, A comparative study of language support for generic programming, in: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, 2003, pp. 115–134. [13] J. Hirschbrunn, Y. Kazakov, Extending description logics with generic concepts – the tale of two
DL Description Logic FOL First-Order Logic ODP Ontology Design Pattern GCI General Concept Inclusion
Theorem 1. There is a non-deterministic algorithm that reduces in polynomial time the second-order satisfiability of a classical ontology with conditional axioms to the classical satisfiability of an ontology potentially including negated axioms.
Given ℐ |=2 , we can construct one such ′ as follows: For each ∈ , we do the following: If is a unit axiom, then ∈ ′ otherwise = { 1, . . . , } ⇒ , and as ℐ |=2 either ∃(1 ≤ ≤ ) : ℐ ̸|= and we add ¬ to ′ or ℐ |= , and we add to ′. Then ℐ |= ′ and because ′ contains the non-conditional axioms of and for each conditional axiom, either one of the negated conditions or the target is in ′, ′ fulfills the construction described above.
Conversely, if ′ is satisfiable then is satisfiable in the same interpretation: Take ℐ such that ℐ |= ′, we show that ℐ |=2 : Take ∈ either is non-conditional and ∈ ′ or = { 1, . . . , } ⇒ and either ∃ : ℐ |= ¬ then ℐ |=2 or ℐ |= and ℐ |=2 .
This gives us a non-deterministic polynomial time reduction.
Lemma 2. Let be a congruence axiom and ℐ a second-order interpretation. Then ℐ |=2 .
able assignment. If ℐ, ̸= ℐ, for some (1 ≤ ≤ ), then, trivially, ℐ |=2 . Otherwise ([1, . . . , ])ℐ, = ℐ (1ℐ, , . . . , ℐ, ) = ℐ (1ℐ, , . . . , ℐ, ) = [1, . . . , ])ℐ, , which, likewise, implies ℐ |=2 . Since was arbitrary, we proved ℐ |=2 .
Lemma 3. Let be a ground ontology and ′ the congruence closure of (see Definition 4). Then is satisfiable under second-order semantics if ′ is (classically) satisfiable.
Proof. (⇒) Let ℐ = (∆ ℐ , · ℐ ) be a second-order interpretation such that ℐ |=2 . Define the classical interpretation = (∆ , · ) with ∆ = ∆ ℐ and [1, . . . , ] = ℐ (1ℐ , . . . , ℐ ) for every ∈ , = ar() and ground L -concepts (1 ≤ ≤ ), and = ℐ for every ∈ . Note that this definition implies that = ℐ for every ground L -concept since the extension of interpretation under concept constructors is defined in ℐ and in the same way. Likewise, ℐ |=2 if |= for every ground L -axiom . Hence, from ℐ |=2 , we obtain |= . Further, by Lemma 2, ℐ |=2 for every congruence axiom ∈ ′. Hence |= ′.
(⇐) Let be a classical interpretation such that |= ′. Define the second-order interpretation ℐ = (∆ ℐ , · ℐ ) with ∆ ℐ = ∆ , ℐ (1, . . . , ) = [1, . . . , ] if [1, . . . , ] ∈ sub() and = (1 ≤ ≤ ), and ℐ (1, . . . , ) = ∅ in the remaining cases, and ℐ = for every ∈ . Notice that the interpretation of (1, . . . , ) is well-defined, i.e., it does not depend on the choice of the atom [1, . . . , ] ∈ sub() such that ℐ = (1 ≤ ≤ ). Indeed, for every other choice [1, . . . , ] ∈ sub() such that = (1 ≤ ≤ ), by Definition 4, the congruence axiom belongs to ′, and since |= ′ and = (1 ≤ ≤ ), we obtain [1, . . . , ] = [1, . . . , ] . Since [1, . . . , ] = ℐ (1ℐ , . . . , ℐ ) for every [1, . . . , ] ∈ sub(), similarly like in the case (⇒), it follows that ℐ |=2 if |= for every ∈ . Since |= ′ and ⊆ ′, it follows that ℐ |=2 .
atoms [1, . . . , ] ∈ sub() is linear in . The statement of the theorem now follows directly from Lemma 3.
Example 1. The following axioms are concept definitions: • 1 = { ⊑ ∃. } ⇒ [ ] ≡ ∃ .( ⊓ [ ]) • 2 = [ ] ≡ ¬ [ ⊓ ] • 3 = [ ] ≡ [[ ⊓ ]] • 4 = [ ] ≡ ¬ • 5 = { ⊑ ∃. } ⇒ [ ] ⊑ [, ] ⊓ ∃. • 6 = { ⊑ [ ], ⊑ [ ]} ⇒ [ ] ⊑ [[]] The following axioms are not: • 1 = [] ≡ ∃ . • 2 = { ⊑ ∃. } ⇒ [ ] ≡ [ ] • 3 = [ ] ≡ ⊓ ∃. • 4 = [] ⊑ ⊥ The sets 1 = { 1, 2} and 2 = { 5, 6} are terminologies, but the set 3 = { 2, 3} is not. Example 2. (Example 1 continued) Take 1 = {[⊥] ≡ ⊥}∪{ 1} this is admissible. Indeed, Conditions 1 and 2 of Definition 7 clearly hold. Condition 3 holds because [⊥] is the only instance of a defined concept appearing in the ground part 1, and for = { ↦→ ⊥}, we have 1 |= ( 1) = {⊥ ⊑ ∃.⊥} ⇒ [⊥] ≡ ∃ (⊥ ⊓ [⊥]). Condition 4 holds because for = ∃.( ⊓ [ ]) and any ℐ ⊆ , we have [ ]ℐ, ⊆ [ ] , for every valuation . Hence ℐ, ⊆ , .
Ontology 2 = { 2} is admissible. We only need to check condition 4. But as is not a defined concept, 1 and 2 interpret exactly the same.
Similarly 3 = { 4} is admissible, as for the same valuation, the interpretation of the description of is always the same.
Ontology 4 = { 1, 2} is not admissible. Again, we only need to check condition 4, but in this case, we have that is indeed a defined concept. So we would need to have that (¬[ ⊓ ])1 ⊆ (¬[ ⊓ ])2 . The interpretation of and is not changed between 1 and 2, but we know that we can have 1 ( ) ⊂ 2 ( ) so in fact we can have (¬[ ⊓ ])1 ⊇ (¬[ ⊓ ])2 and the condition does not hold.
Similarly, ontology 5 = { 1, 3} is not admissible. This is because, again, we do not have monotonicity of the description of . Realize that 1 (1 ( )) ⊆ 2 (2 ( )) does not necessarily hold, because we only know that 1 ( ) ⊆ 2 ( ) holds for the same not for diferent ones. In fact, if we add the axiom 4 (which is admissible on its own) to 5, we get 5 |=2 4.
Proof. Given a model ℐ = (∆ ℐ , · ℐ ) of , we show that the fixpoint of 1Exp,ℐ exists and is a model of .
1Exp(2). By Definition 8, we need to show 1Exp(1)(1, . . . , ) ⊆ 1Exp(2)(1, . . . , ) for all unknown 1, . . . , ⊆ ∆ ℐ . Let = { → } then by Definition 7 Case 4, 1, ⊆ 2, and (1, . . . , )1Exp(1) = 1, ⊆ 2, = 1Exp(2)(1, . . . , ).
[
We now show that |=2 . Take Γ ⇒ ∈ and some , we show that |=2 Γ ⇒ . If ̸|=2 Γ , we are finished. Otherwise, we show that |=2 . Assume that (partially) defines [1, . . . , ]. If we have [1, . . . , ] ∈ sub() and () = (1 ≤ ≤ ), then by Definition 7 Case 3, |=2 [1/1, . . . , /]( ) and as |=2 , |=2 . Otherwise, if = [1, . . . , ] ⊑ , then by Definition 6, [1, . . . , ] , = ∅ and therefore |=2 . Finally, if = [1, . . . , ] ≡ , because is a fixpoint of the one-step expansion, we know that applying the one-step expansion to does not change the interpretation of . Then we know that for the interpretation of [1, . . . , ] this means that [1, . . . , ] , = , and |=2 .
Therefore, we have shown that there is a model such that |= .