The study of Description Logics have been historically mostly focused on features that can be translated to decidable fragments of first-order logic. In this paper, we leave this restriction behind and look for useful and decidable extensions outside first-order logic. We introduce universally quantified concepts, which take the form of variables that can be replaced with arbitrary concepts, and define two semantics of this extension. A schema semantics allows replacements of concept variables only by concepts from a particular language, giving us axiom schemata similar to modal logics. A second-order semantics allows replacement of concept variables with arbitrary subsets of the domain, which is similar to quantified predicates in second-order logic. To study the proposed semantics, we focus on the extension of the description logic ℰℒ. We show that for a useful fragment of the extension, the conclusions entailed by the diferent semantics coincide, allowing us to use classical ℰℒ reasoning algorithms even for the second-order semantics. For a slightly smaller, but still useful, fragment, we were also able to show polynomial decidability of the extension. This fragment, in particular, can express a generalized form of role chain axioms, positive self restrictions, and some forms of (local) role-value-maps from KL-ONE, without requiring any additional constructors.
After the famous undecidability result of the early knowledge representation language used in
the KL-ONE system [
One possible way of defining semantics of our language extension, is to regard axioms with concept variables as axiom schemata. Under this reading, the reasonable choices of in the above axiom, are sets defined by concepts of a specific form, for example, all (atomic) concepts from an ontology, or all concepts that can be built in a particular DL, such as ℰ ℒ. After replacing each variable with every possible concept, one obtains a (possibly infinite) set of ordinary DL axioms, for which the logical entailment is defined in the standard way.
Axiom schemata is certainly not a new concept. In fact, most logic languages, including
Propositional Logic (PL), FOL, and Modal Logics (MLs) were originally defined axiomatically.
For example, PL can be defined using 3 axiom schemata: → , → ( → ), and
( → ( → )) → (( → ) → ( → )), in which every variable can be replaced with
any propositional formula. Many MLs were defined by extending PL with new axiom schemata,
for example, K4: □ → □ (see, e.g., [6]). In the context of DLs, axiom schemata occur in
diferent contexts: Nominal Schemas [ 7, 8, 9] introduce (nominal) variables that can be replaced
with individual names. Ontology Design Patterns (ODPs) [
The main advantage of the schema semantics for concept variables, is that any DL reasoning procedure could, in principle, be used for checking entailment in the corresponding DL extension, by systematically generating instances of axiom schemata and checking entailment from the resulting increasing sets of ordinary axioms. This immediately implies semi-decidability of the schema extension and, in the cases when a form of sub-formula property can be proved, also decidability and complexity results. Schema semantics, however, also has disadvantages, one of which, is that the entailments depend on the choices of concepts used for variable replacements. Consider, for example, axiom schema ⊤ ⊑ ∃.. If we only allow ℰ ℒ concepts for variable replacements, the resulting set of axioms is satisfiable since there is a model (with one element) that interprets every ℰ ℒ concept (including every ∃.) by the whole domain. If, however, we additionally allow to be replaced by ⊥, i.e., by taking concepts from ℰ ℒ⊥, then, clearly, this schema becomes unsatisfiable. As a consequence, the ℰ ℒ axiom schema obtains new ℰ ℒ logical conclusions (e.g., ⊑ ) when viewing it in a context of a larger language (e.g., ℰ ℒ⊥). In the next section we give a similar example when an ℰ ℒ schema obtains new ℰ ℒ consequences with ℒ concept replacements, this time, without making axioms inconsistent.1
Motivated by the above consideration, we define another, language-independent semantics of concept variables. Specifically, an axiom with concept variables is satisfied by an interpretation if for every assignment of concept variables to subsets of its domain, the axiom is satisfied in the extension of this interpretation in which the variables are interpreted by these subsets (as 1To see why this could be a concern, imagine that the axiom schemata of PL would obtain new logical consequences in the language of PL when allowing variables to be replaced by modal formulas! ordinary concept names). For example, axiom ⊤ ⊑ ∃. is not satisfied in any interpretation ℐ since for the assignment of ↦→ ∅, this axiom does not hold if we extend ℐ by ℐ = ∅. On the other hand, axiom ⊑ ∃. is satisfied in exactly those interpretations ℐ such that ℐ is a reflexive relation. Similarly, axiom ∃owns.( ⊓ Pet) ⊑ ∃feeds. is satisfied in exactly those interpretations ℐ such that ⟨, ⟩ ∈ ownsℐ and ∈ Petℐ imply ⟨, ⟩ ∈ feedsℐ .2 Essentially, under this semantics, concept variables correspond to universally-quantified second-order (unary) predicates. Hence, we refer to this semantics as second-order semantics.
It is easy to see that the second-order semantics is stronger than the schema semantics. Indeed,
if an axiom is satisfied in an interpretation under the second-order semantics, then for every
replacement of variables by concepts, the resulting axioms are also (classically) satisfied in
this interpretation because variables can be assigned to interpretations of these concepts in
the second-order semantics. The converse is not true, as has been shown on the example of
axiom ⊤ ⊑ ∃. for the ℰ ℒ-schema semantics. Furthermore, whereas schema entailment
can be always reduced to first-order entailment (from possibly infinite set of formulas), there
are axioms whose models under second-order semantics cannot be expressed by first-order
formulas. For example, the well-known ML McKinsey axiom □♢ → ♢□ , which can be
written in the DL ℒ as ∀.∃. ⊑ ∃.∀., cannot be translated into even an infinite set
of first-order formulas that holds in exactly the same interpretations (of ) [
To combine advantages of the two proposed semantics (semi-decidability and schema language independence), it makes sense to look for restricted use of concept variables in DLs for which the entailment under two semantics coincide. In this paper, we describe a useful extension of the DL ℰ ℒ with concept variables for which this is the case (Section 3), and a further restriction, for which these (equivalent) entailments are polynomially decidable (Section 4). Even though the use of concept variables in this fragment is restricted, it could express several other DL features, such as role chain axioms, positive self restrictions, including reflexive roles, some forms of (local) role-value-maps from KL-ONE, and their generalizations (see Section 5).
The main idea for proving these results, is to show that the standard ℰ ℒ canonical model [2] for axioms obtained by replacing concept variables with certain relevant ℰ ℒ concepts, is also a model of the original axioms under the second-order semantics. This property holds because for our restricted form of axioms, it is suficient to replace concept variables with only singleton subsets of the domain to capture the second-order semantics.3 For example, if ⊑ ∃. holds for all replacements of with singleton subsets of the domain (that is, when is reflexive) then this axiom also holds for replacements of with any larger set. To obtain the decidability and complexity result, we define a further restriction for which it is suficient to use only polynomially-many relevant concepts for checking the schema entailment.
Because of limited space, we omit most proofs in this paper. They can be found in the
accompanying technical report [
We start by formally defining our extension of DLs with concept variables: Definition 1 (Syntax). The syntax of DLs with concept variables consists of disjoint and countably infinite sets of concept names, of role names, and of concept variables. Given a base DL L that is a fragment of ℛℐ, such as ℰ ℒ and ℒ, we define by L its corresponding extension with concept variables, in which the elements from can be used as concepts. We define, an L -ontology as a (possibly infinite) set of L -axioms.
Let ex be either an L -concept, an L -axiom, or an L -ontology. We denote by sub(ex) (all) subconcepts4 of ex. For L -concepts and L -axioms, we split sub(ex) into sub+(ex) and sub− (ex) the set of concepts that occur positively, respectively negatively in ex5 (i.e. sub(ex) = sub+(ex) ∪ sub− (ex)). We denote by vars(ex) = sub(ex) ∩ the set of concept variables occurring in ex. We say that ex is ground if vars(ex) = ∅.
A (concept variable) substitution is a mapping = [1/1, . . . , /] that assigns concepts to concept variables (1 ≤ ≤ ). We say that is ground if all are ground (1 ≤ ≤ ). We denote by (ex) the result of applying the substitution to ex, defined in the usual way.
From now on we assume that DL concepts, axioms, and ontologies may contain concept variables. When this is not the case, we explicitly say that these concepts, axioms, or ontologies are ground or classical.
Example 1. Consider the following two (non-ground) axioms: = ∃. ⊓ ∃. ⊑ ∃., = ∃. ⊓ ∃. ⊑ ∃.( ⊔ ).
Axiom belongs to ℰ ℒ whereas axiom belongs to ℒ due to the use of concept disjunction ⊔. Further, sub+( ) = {∃., }, sub− ( ) = {∃. ⊓∃., ∃., ∃., , }, and vars( ) = {, }. Finally, for a (non-ground) substitution = [/ ⊔ ], we have:
( ) = ∃.( ⊔ ) ⊔ ∃( ⊔ ) ⊑ ∃.( ⊔ ).
Intuitively, axioms and can be thought as axiom schemata representing all axioms obtained by replacing the concept variables and with ordinary (ground) concepts. However, the choice of such ground concepts is not always obvious. Should variables be replaced by just atomic concepts? Or only by concepts appearing in the given ontology? Or by any concepts that can be constructed in a particular DL? Clearly, each of these choices may result in diferent logical consequences and algorithmic properties of the resulting schema languages. To handle all such choices, we provide a general (parameterized) definition of schema semantics. Definition 2 (Schema Semantics). Let be an L -ontology for some DL L, and a (possibly infinite) set of L-concepts called a concept base. For an L -axiom , and L -ontology , define 4Subconcepts are defined to be substrings of the expression that are valid concepts. 5A concept occurs positively (negatively) in an axiom, if it occurs on the right side of the axiom under even (odd) number of nested negations or on the left side under odd (even) number of nested negations. (1) (2) (3) by ↓ = { [1/1, . . . /] | ∈ vars( ) & ∈ } and ↓ = ⋃︀ ∈ ↓ the set of -ground instances of and , respectively.
We write |=* if ↓ |= ↓ and say that is a logical consequence of under the schema semantics (for a concept base ). Finally, we write ↓L, ↓L and |=*L instead of ↓ , ↓ and |=* , respectively, if is the set of all L-concepts.
Clearly, if the concept base is finite , entailment under the schema semantics for can be reduced to the standard DL entailment.
Example 2 (Example 1 Continued). Notice that { } |=* for any concept base . Indeed, take any ′ = ( ) = ∃. ⊓ ∃. ⊑ ∃. ∈ ↓ . Then ↓ ∋ [/, /] = ∃. ⊓ ∃. ⊑ ∃.( ⊔ ) |= ′. Also, notice that if is closed under concept disjunctions (i.e., ∈ and ∈ imply ⊔ ∈ ) then { } |=* . Indeed, take any ′ = ( ) = ∃. ⊓ ∃. ⊑ ∃.( ⊔ ) ∈ ↓ for = [/, /]. Since is closed under disjunction, we have ↓ ∋ [/ ⊔ ] = ∃.( ⊔ ) ⊓ ∃.( ⊔ ) ⊑ ∃.( ⊔ ) |= ′. Consequently, { } |=*ℒ . However, it can be shown that { } ̸|=*ℰℒ . To prove this, consider the ℰ ℒ ontology: = { ⊑ ∃. ⊓ ∃., ∃. ⊑ , ∃. ⊑ } (4) It is easy to see that ∪ ↓ℰℒ ⊇ ∪ { ′} |= ⊑ for ′ = [/, /] = ∃. ⊓ ∃. ⊑ ∃( ⊔ ). Hence ∪ { } |=*ℰℒ ⊑ . We show that ∪ { } ̸|=*ℰℒ ⊑ , which, in particular, implies that { } ̸|=*ℰℒ , for otherwise ∪ { } |=*ℰℒ ∪ { } |=*ℰℒ ⊑ .
To prove that ∪ { } ̸|=*ℰℒ ⊑ , consider the interpretation ℐ = (∆ ℐ , · ℐ ) defined by: ∆ ℐ = {, , }, ℐ = {}, ℐ = {}, ℐ = {}, ℐ = {⟨, ⟩}, ℐ = {⟨, ⟩}, ℐ = {⟨, ⟩}, and ℐ = ℎℐ = ∅ for all remaining ∈ and ℎ ∈ . Clearly, ℐ |= and ℐ ̸|= ⊑ . It remains to prove that ℐ |= ↓ℰℒ. Take any [/ ] = ∃. ⊓ ∃. ∈ ∃. ∈ ↓ℰℒ and any ∈ (∃. ⊓ ∃. )ℐ . Then = and {, } ⊆ ℐ by definition of ℐ and ℐ . But then = ⊤ since || ℐ || ≤ 1 for all other ℰ ℒ concepts . Then = ∈ (∃.⊤)ℐ = (∃. )ℐ as required.
Combining the above observations, we obtain: ∪ { } |=*ℒ ∪ { } |=*ℰℒ ∪ { } |=*ℰℒ ⊑ , however, ∪ { } ̸|=*ℰℒ ⊑ .
Example 2 shows that, for schema semantics, an ontology formulated in one DL may have diferent conclusions, even in the same DL, when the concept base is extended to a larger language. This goes against the usual understanding of logic, as this means that the consequences of an ontology are not determined by the ontology alone. To mitigate this problem, we consider the second-order semantics that is independent of a concept base.
Definition 3 (Second-Order Semantics). Let ℐ = (∆ ℐ , · ℐ ) be an interpretation. A valuation for ℐ (also called a variable assignment) is a mapping that assigns to every variable ∈ a subset () ⊆ ∆ ℐ . The interpretation of concepts ℐ, and satisfaction of axioms ℐ |=2 under ℐ and is defined in the same way as for the standard DL semantics by treating concept variables as ordinary concept names interpreted by (). 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 .
Alternatively to the model-theoretic definition (Definition 3) it is possible to define the second-order semantics by a translation to SOL. This translation is simply the normal translation to FOL, treating concept variables as second-order unary predicates and then universally quantifying over these predicates. For example, ⊑ ∃. ⊓ translates to ∀.∀.[∀.(() → ∃.((, ) ∧ ()) ∧ ())].
As discussed in Section 1, second order semantics is stronger than schema semantics. Let us consider some examples for the DL ℰ ℒ, which have more second order entailments than schema semantics for which all ℰ ℒ concepts are included in the concept base. These examples will help us to determine the restrictions for the use of concept variables, under which both semantics coincide.
First, we give a minor modification of the example with axiom ⊤ ⊑ ∃. discussed in Section 1, which does not result in an inconsistent ontology under the second-order semantics. Example 3. Consider the ontology = { ⊑ ∃.}. It is easy to see that |=2 ∃. ⊑ . Indeed, assume that ℐ |=2 , and take any valuation such that () = ∅. Then ℐ = ℐ, ⊆ (∃.)ℐ, = ∅. Hence (∃.)ℐ = ∅ ⊆ ℐ . At the same time ̸|=*ℰℒ ∃. ⊑ . Indeed, consider the interpretation ℐ = (∆ ℐ , · ℐ ) with ∆ ℐ = {, }, ℐ = {}, ℐ = {, } for every ∈ ∖ {}, and ℐ = {⟨, ⟩, ⟨, ⟩} for every ∈ . By structural induction, it is easy to show that ∈ ℐ for every ℰ ℒ concept , hence ℐ |= ⊑ ∃.. Therefore, ℐ |=*ℰℒ . However, since (∃.)ℐ = {, } ̸⊆ { } = ℐ , we obtain ̸|=*ℰℒ ∃. ⊑ .
Example 3 can be generalized to many other ℰ ℒ axioms ⊑ for which there exists a concept variable appearing in but not in . In this case, ℐ |=2 ⊑ implies that ℐ, = ∅ for every valuation because for the extension ′ of with ′() = ∅, we obtain ℐ, = ℐ, ′ ⊆ ℐ, ′ = ∅.
Now, take any ℐ |=2 ⊑ . Then ℐ, = ∅ for every valuation . Then ()ℐ = ∅ for every concept variable substitution . Then for every ℰ ℒ concept such that () ∈ sub() we have ℐ = ∅ as well. Thus { ⊑ } |=2 ⊑ for every . If the schema semantics preserves all these entailments then, in particular, all such concepts (containing instances of ) must be equivalent. This can happen only in some trivial cases, e.g., when the contains axiom of the form ⊑ , which implies that all concepts are equivalent. To ensure that the semantics coincide in non-trivial cases, it is, therefore, make sense to require that all variables that are present on the right side of a concept inclusion axioms are also present on the left side. Axioms that fulfill this requirement we called range restricted axioms.
Example 2 presents another situation when schema semantics gives fewer consequences than the second-order semantics. As has been shown in this example, for an ℰ ℒ axiom (1) and an ℰ ℒ ontology from (4), we have ∪ { } ̸|=* ⊑ , however, since { } |=*ℒ (2) and ∪ { } |=*ℰℒ ⊑ , we have ∪ { } |=2 ℰℒ⊑ .
The problem with in this example is that the variable occurs twice on the left side of the axiom, which makes this axiom equivalent to under the second-order semantics, and, consequently, being able to express an axiom with a concept disjunction ∃. ⊓ ∃. ⊑ ∃.( ⊔ ), which otherwise could not be expressed by ordinary ℰ ℒ axioms, i.e., under the schema semantics. To prevent such a case for our fragment of ℰ ℒ , it therefore, makes sense to prohibit the occurrence of the same variable twice on the left side of an axiom. Concepts in which each variable occurs at most once, we call linear.
To motivate our last restriction, consider the next example.
Example 4. Consider the ℰ ℒ ontology = {∃. ⊑ ∃.( ⊓ )}. It is easy to see that |=2 ∃.⊤ ⊑ ∃.. Indeed, take any ℐ |=2 and ∈ (∃.⊤)ℐ . Then there exists ′ ∈ ∆ ℐ such that ⟨, ′⟩ ∈ ℐ . Take any valuation with () = {′}. Since ⟨, ′⟩ ∈ ℐ , we have ∈ (∃.)ℐ, . Since ℐ | , we have ∈ (∃.( ⊓ ))ℐ, . In particular, ∅ ̸= ( ⊓ )ℐ, = {′} ∩ ℐ . Hence =2 ′ ∈ ℐ . Consequently, ∈ (∃.)ℐ .
On the other hand, ̸|=*ℰℒ ∃.⊤ ⊑ ∃., as evidenced by the counter-model ℐ = (∆ ℐ , · ℐ ) with ∆ ℐ = {, }, ℐ = {}, ℐ = {⟨, ⟩}, ℐ = {⟨, ⟩}, and ℐ = ∅, ℎℐ = ∅ for any remaining ∈ and ℎ ∈ . To show that ℐ |=*ℰℒ , we prove that ℐ |= ∃. ⊑ ∃.( ⊑ ) for every ℰ ℒ concept . For this, take any ∈ (∃.)ℐ . By definition of ℐ , = and ∈ ℐ . Then can be only a conjunction of concept ⊤. Hence ∈ . Hence = ∈ (∃.)ℐ . Thus ℐ |= . Since, ∈ (∃.⊤)ℐ but (∃.)ℐ = ∅, we proved that ̸|=*ℰℒ ∃.⊤ ⊑ ∃..
Note that under the second order semantics, the axiom ∃. ⊑ ∃.( ⊓ ) in from
Example 4 implies two properties: (1) that is a subrole of ( ⊑ ), which is equivalent to
axiom ∃. ⊑ ∃., and (2) that is a range of the role (() ⊑ ), which is due to the
fact that for any element ′ such that ⟨, ′⟩ ∈ ℐ this axiom holds for = {′}. As was shown
in the example, the schema semantics cannot capture the second kind of properties. In fact, an
extension of ℰ ℒ with both (complex) role inclusions and range restrictions becomes undecidable
[
In this section we prove that the restrictions on the use of concept variables discussed in Section 2 are suficient to guarantee that the logical consequences under the schema semantics and second-order semantics coincide. Towards this goal, we define a fragment ℰ ℒ 1 of ℰ ℒ that satisfies these restrictions: Definition 5 (ℰ ℒ 1). A ℰ ℒ axiom = ⊑ is in the fragment ℰ ℒ 1, if • is range restricted, i.e. vars() ⊆ vars(), • is linear, i.e. it does not contain a variable twice, and • is safe (cf. Definition 4),
An interesting consequence of the first two restrictions in Definition 5, is the so-called singleton property for valuations. Intuitively, for checking entailment over the second-order semantics, it is suficient to consider only valuations that assign concept variables to singleton subsets of the domain.
Definition 6 (Singleton Valuation). A valuation is a singleton valuation if ∀ : || ()|| = 1. Lemma 1. Let ℐ be an interpretation, a linear ℰ ℒ concept, a valuation, and ∈ ℐ, . Then there is a singleton valuation ′ such that ′() ⊆ () for every ∈ vars() and ∈ ℐ, ′ . Lemma 2. Let ℐ be an interpretation, an ℰ ℒ concept, and ′, valuations such that ′() ⊆ () for every ∈ vars(). Then ℐ, ′ ⊆ ℐ, .
By combining the above two lemmata, we obtain the required singleton property: Theorem 1 (Singleton Property). Let ℐ be an interpretation, = ⊑ a range restricted ℰ ℒ axiom such that is linear, and ℐ |=2′ for every singleton valuation ′. Then ℐ |=2 .
Our next goal is to prove that if |=2 for some ℰ ℒ 1 ontology and a (ground) ℰ ℒ
axiom , then |=* for some concept base consisting of (ground) ℰ ℒ concepts, i.e.,
↓ |= (cf. Definition 2). Since ↓ is an ordinary ℰ ℒ ontology, we can use the well known
characterization of ℰ ℒ entailment using so-called ℰ ℒ canonical models (also called completion
graphs [2]). Usually canonical models are defined using consequences of the ontology derived by
certain inference rules (see, e.g., [
If we include all ℰ ℒ concepts into the concept base , it can be shown that the canonical interpretation ℐ is a model of that satisfies exactly ℰ ℒ axioms entailed by : ℐ |= if |= . However, to ensure the latter property for a fixed , it is suficient to use a smaller concept base that contains only certain sub-concepts of and . It turns out that if satisfies certain conditions for = ↓ and then |=2 implies ℐ |= , which implies |= . To prove that ℐ |= , we show that ℐ |=2 , for which we use the singleton valuation property from Theorem 1. There is a nice connection between singleton valuations in ℐ and substitutions of concept variables with concepts from , which we are going to exploit.
Definition 8 (Canonical Substitution). We say that a concept variable substitution is canonical for a concept base , if () ∈ for every ∈ . Given a canonical interpretation ℐ (for and ) and a singleton valuation for ℐ, the canonical substitution determined by is the substitution = defined by () = if () = { } ⊆ ∆ ℐ .
The connection to canonical substitutions in Definition 8 helps us to characterize interpretations of (complex) ℰ ℒ concepts under canonical models and singleton valuations. Lemma 3. Let ℐ be the canonical interpretation w.r.t. some ℰ ℒ ontology and a concept base , an ℰ ℒ concept, a singleton valuation, and = the corresponding canonical substitution. Then: In addition, if is a safe concpet (see Definition 4) and () ∈ for every ∃. ∈ sub( ) then ℐ, ⊆ { ∈ ∆ ℐ | |= ⊑ ( )}. ℐ, ⊇ { ∈ ∆ ℐ | |= ⊑ ( )}. (5) (6)
The restriction to safe concepts in Lemma 3 is necessary, as the following example shows: Example 5. Consider = {, } ⊆ and = { ⊑ }. Then the canonical interpretation ℐ for and has domain ∆ ℐ = {, } and assigns ℐ = {, }, ℐ = {}. Now take = ∈ and define a singleton () = {}. Then the corresponding canonical substitution () = . As can be seen, ℐ, = () = {} ⊊ {, } = { ∈ ∆ ℐ | |= ⊑ }.
We are now ready to harvest the fruits of our characterization of canonical interpretations. We first show that, the canonical interpretation cannot entail more axioms than the ontology for which it is constructed if the concept base contains relevant concepts from these axioms. Corollary 1. Let ℐ be the canonical interpretation w.r.t. and , and = ⊑ an ℰ ℒ axiom such that ∈ and ∈ for every ∃. ∈ sub( ). Then ℐ |= implies |= . Proof. By Lemma 3, ℐ ⊆ { ∈ ∆ ℐ | |= ⊑ } and ℐ ⊇ { ∈ ∆ ℐ | |= ⊑ } Since |= ⊑ and ∈ , we have ∈ ℐ . Since ℐ |= ⊑ , we have ∈ ℐ ⊆ { ∈ ∆ ℐ | |= ⊑ }. Hence |= ⊑ .
Next, we determine what to put into and so that the canonical interpretation ℐ = ℐ(, ) satisfies a given ℰ ℒ axiom (to eventually ensure that ℐ |= ).
Corollary 2. Let ℐ be the canonical interpretation w.r.t. and , and = ⊑ an ℰ ℒ 1 axiom such that 1) ↓ ∈ and 2) ↓ ⊆ for every ∃. ∈ sub(). Then ℐ |=2 .
By combining Corollary 1 and Corollary 2, for the given ℰ ℒ 1 ontology and an ℰ ℒ axiom , we can define the smallest concept base such that the canonical interpretation ℐ w.r.t. for = ↓ and satisfies all axioms ∈ under the second-order semantics and entails only if |= and thus only if |=* . Note that Condition 2) in Corollary 2 is recursive over . Therefore, the required is defined as a fixed point limit for this condition. Definition 9 (Expansion & Expansion Base). Let be a ℰ ℒ ontology and = ⊑ an ℰ ℒ axiom. Let 0 = { } ∪ { | ∃. ∈ sub( )}, and +1 = ∪ ⋃︀∃.∈sub+() ↓ for ≥ 0. We call ∞ = ⋃︀≥ 0 the expansion base and = ↓∞ the expansion for w.r.t .
We show that the expansion base ∞ is indeed a fixed point of the required condition: Lemma 4. Let ∞ be the expansion base for w.r.t . Then ↓∞ ⊆ ∞ for every ∃. ∈ sub+().
By combining Corollary 1, Corollary 2 and Lemma 4, we now prove the following result: Theorem 2. Let be an ℰ ℒ 1 ontology, an ℰ ℒ axiom, and ∞ the expansion of w.r.t. . Then |=2 implies ∞ |= .
An immediate consequence of Theorem 2 is that the schema semantics coincides with secondorder semantics for ℰ ℒ 1 ontologies.
Theorem 3. Let be a ℰ ℒ 1 ontology and an ℰ ℒ axiom. Then |=2 ⇔ |=*ℰℒ .
Because the schema semantics and the second-order semantics coincide for ℰ ℒ 1, we
immediately obtain semi-decidability of the entailment for the latter. In general, entailment in
ℰ ℒ 1 ist still undecidable because ℰ ℒ 1 can express (unrestricted) role-value-maps:
Definition 10 (Role-Value-Maps). A role-value-map [
Lemma 5. For every interpretation ℐ it holds ℐ |=2 ∃1.∃2. . . . ∃. ⊑ ∃1.∃2. . . . ∃. if 1ℐ ∘ · · · ∘ ℐ ⊆ 1ℐ ∘ · · · ∘ ℐ.
Theorem 4. Axiom entailment in ℰ ℒ 1 is undecidable.
Proof. Follows directly from Lemma 5 and the fact that axiom entailment is undecidable in ℰ ℒ
extended with role-value-maps [
The reason for this undecidiblity, is deep nesting of concept variables on the right side of axioms under existential restrictions. Such nested variables result in infinite expansion base ∞ as the following example shows: Example 6. Consider the ℰ ℒ 1 ontology = { ⊑ ∃.∃.} and = ⊑ . Then according to Definition 9, we have 1 = {}, 1 = { ⊑ ∃.∃.}, 2 = {, ∃.}, 2 = { ⊑ ∃.∃., ∃. ⊑ ∃.∃.∃.}, 3 = {, ∃., ∃.∃.}, etc.
If we restrict ℰ ℒ 1 so that variables on the right side do not appear under nested existential restrictions, we can show that the expansion ∞ of the ontology is, in fact, polynomial in the size of , which gives us polynomial decidability of the (schema and second-order) entailment. Definition 11 (ℰ ℒ 2). An ℰ ℒ 2 axiom is an ℰ ℒ 1 axiom such that for every ∃. ∈ sub+( ), either = ∈ or vars() = ∅.
Lemma 6. Let be an ℰ ℒ 2 ontology, an ℰ ℒ axiom and ∞ the expansion base for and . Then ∞ = 0 ∪ { | ∃. ∈ sub+() & vars() = ∅}.
Since the elements of ∞ are subsets of (ground) concepts appearing in and , we obtain: Theorem 5. Let be a ℰ ℒ 2 ontology and an ℰ ℒ axiom. Then the entailment |=2 is decidable in polynomial time in the size of and .
In this paper, we left behind the usual restriction of DLs to fragments of FOL and introduced concept variables directly into DLs. These concept variables can be understood as simple placeholders for concrete concepts, giving us axiom schemas. This results in a semantics that replaces variables by a specific set of concepts and in this way reduces reasoning to the classical case. Or they can be understood more strongly, as universally quantified concepts, similar to predicates in SOL. This gives us a semantics that interprets variables as arbitrary subsets of the interpretation domain and results in the DL being a fragment of SOL.
We applied this extension to ℰ ℒ and analyzed the diference in entailed conclusions by the two semantics. We defined a fragment for which the conclusions coincide, given us semi-decidability also for second-order semantics. We also showed that for a slight limitation of this fragment, second-order semantics (and schema semantics) even become decidable.
In this decidable fragment ℰ ℒ 2, we can express a range of features that usually require
special constructors in classical ℰ ℒ: We can express role chain axioms that reduce a chain of
roles to a connection via one role. What would normally be expressed as 1 ∘ · · · ∘ ⊑
(i.e. role-value-maps where the right side is a single role, cf. Definition 10), we can express
as ∃1.∃2. . . . ∃. ⊑ ∃.. For example father ∘ father ⊑ grandfather is equivalent to
∃father.∃father. ⊑ ∃grandfather.. We can also express self restrictions on the right side of
axioms, i.e. classical axioms of the form ⊑ ∃.Self, meaning ∀ : ( ∈ ℐ ) ⇒ (⟨, ⟩ ∈ ℐ )
(cf. e.g. [
It is possible to generalize Theorem 3 and Theorem 5 to entailments of arbitrary ℰ ℒ axioms because such entailments can be always reduced to entailment of ℰ ℒ axioms by simply replacing all concept variables in with new atomic concepts, not occurring in or . Intuitively, to prove that every (second order or schema) model of the ontology satisfies under each valuation or substitution , we can extend this model by interpreting the new atomic concepts according to the value of () or () on the variables which they replace. This still remains a model of the ontology since it does not contain these new concepts.
Summarizing, the results in this paper show that an extension of DLs to being fragments of SOL, instead of FOL, is possible (while remaining decidable for reasonable restrictions) and does allow expressing facts in a new way without the use of special constructors. This enlightens the relationship between FOL, SOL and DLs and opens the way for further extensions of DLs outside FOL. of Knowledge Representation and Reasoning (KR’89). Toronto, Canada, May 15-18 1989, Morgan Kaufmann, 1989, pp. 421–431. [2] F. Baader, S. Brandt, C. Lutz, Pushing the EL Envelope, LTCS-Report LTCS-05-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2005. doi:https://doi.org/10.25368/2022.144, see http://lat.inf.tu-dresden.de/research/reports.html. [3] D. Calvanese, G. D. Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Tractable reasoning and eficient query answering in description logics: The DL-Lite family, J. of Automated Reasoning 39 (2007) 385–429. [4] I. Horrocks, O. Kutz, U. Sattler, The even more irresistible SROIQ, in: P. Doherty, J. Mylopoulos, C. A. Welty (Eds.), Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006, AAAI Press, 2006, pp. 57–67. URL: http://www.aaai.org/Library/KR/2006/kr06-009.php. [5] B. Motik, P. F. Patel-Schneider, B. Cuenca Grau (Eds.), OWL 2 Web Ontology Language: Direct Semantics, W3C Recommendation, 27 October 2009. Available at http://www.w3. org/TR/owl2-direct-semantics/. [6] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001. URL: https://doi.org/10. 1017/CBO9781107050884. doi:10.1017/CBO9781107050884. [7] D. Carral, J. Zalewski, P. Hitzler, An eficient algorithm for reasoning over OWL EL ontologies with nominal schemas, J. Log. Comput. 33 (2023) 136–162. URL: https://doi.org/ 10.1093/logcom/exac032. doi:10.1093/logcom/exac032. [8] M. Krötzsch, F. Maier, A. Krisnadhi, P. Hitzler, A better uncle for OWL: nominal schemas for integrating rules and ontologies, in: S. Srinivasan, K. Ramamritham, A. Kumar, M. P. Ravindra, E. Bertino, R. Kumar (Eds.), Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, ACM, 2011, pp. 645–654. URL: https://doi.org/10.1145/1963405.1963496. doi:10.1145/1963405. 1963496. [9] D. Carral, C. Wang, P. Hitzler, Towards an eficient algorithm to reason over description logics extended with nominal schemas, in: Web Reasoning and Rule Systems: 7th International Conference, RR 2013, Mannheim, Germany, July 27-29, 2013. Proceedings 7, Springer, 2013, pp. 65–79. [10] 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, CEUR-WS.org, 2015. URL: https://ceur-ws.org/Vol-1515/demo2.pdf. [11] 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. Kaffee, 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. [12] C. Kindermann, D. P. Lupp, U. Sattler, E. Thorstensen, Generating ontologies from tem