We present a second-order language that can be used to succinctly specify ontologies in a consistent and transparent manner. This language is based on ontology templates (OTTR), a framework for capturing recurring patterns of axioms in ontological modelling. The language, and our results are independent of any specific DL. We define the language and its semantics, including the case of negation-asfailure, investigate reasoning over ontologies specified using our language, and show results about the decidability of useful reasoning tasks about the language itself. We also state and discuss some open problems that we believe to be of interest.
The phenomenon of frequently occurring structures in ontologies engineering
(OE) has received attention from a variety of angles. One of the first accounts is
given in [
In this paper, we propose a new language that allows expressing patterns of repeated structures in ontologies. This language is rule-based and has both a model-theoretic and a fixpoint semantics, which we show coincide. In contrast to other rule languages “on top of” DLs, in this language firing a rule results in the addition of TBox and/or ABox axioms. The goal is to succinctly describe ontologies, thereby making them more readable and maintainable.
Given that DL ontologies are sets of axioms, an ontology provides no means to arrange its axioms in a convenient manner for ontology engineers. In particular, it is not possible to group conceptually related axioms or indicate interdependencies between axioms. While ontology editors such as Protégé3 display an ontology through a hierarchy of its entities, conceptual interdependencies between axioms are hidden and the underlying structural design of an ontology remains obscured.
1 = {Jaguar ⊑ Animal,
(1) (2) (3) Then, an ontology editor will group the entities Jaguar, Tiger and Lion under Animal according to their class hierarchy.
However, 1 contains no indication that every subclass of Animal can have only children of the same class . Assume this regularity is no coincidence but a desired pattern that should hold for any subclass of Animal. Currently, ontology engineers have no means of expressing or enforcing such a pattern other than dealing with the ontology as a whole, inspecting all axioms separately, and making necessary changes manually.
Expressing patterns such as in Example 1 explicitly has a potential to reveal some aspects of the intentions for the design of an ontology.
2 = {Jaguar ⊑ Animal, Tiger ⊑ Animal, Lion ⊑ Animal}
Bod⏞y : {? ⊑ Animal} → {? ⊑ ∀hasChild.?}, ⏟ ⏟
Hea⏞d where ? is a variable. We can interpret the body of this rule as a query which, when evaluated over the ontology 2, returns substitutions from the signature of 2 for ?. These substitutions can then be used to instantiate the axioms in the head of the rule. Firing the above rule over 2 would add all those resulting axioms to 2, thereby reconstructing 1 from Example 1.
In the following, we will call such rules generators. The possible benefits of generators are threefold. Firstly, 2 in combination with is easier to understand because makes a statement about all subconcepts of Animal that the type of an animal determines the type of its children. This is a kind of meta-statement about concepts which a user of an ontology can usually only learn by inspecting (many) axioms in an ontology. Secondly, 2 in combination with is easier to maintain and extend compared to 1, where a user would have to manually ensure that the meta-statement continues to be satisfied after new concepts have been added. 3 https://protege.stanford.edu/ Thirdly, conceptual relationships captured in a generator such as are easy to reuse and can foster interoperability between ontologies in the spirit of ontology design patterns.
This paper is accompanied by a more detailed technical report [
Let , , and be sets of individual, concept, and role names, each containing
a distinguished subset of individual, concept, and role variables , , and .
A concept (resp. role) is either a concept name (resp. role name) or a concept
expression (resp. role expression) built using the usual DL constructors [
A template is an ontology, and we write ( ) for ⊆ ∪ ∪ the set of variables occurring in . As the variables are concept, role, and individual names, the semantics of a template is the same as of a regular ontology. For the sake of brevity, we occasionally omit the variable set when it is either clear from context or nonvital to the discussion. Templates can be instantiated by applying a substitution to them. A substitution is a function that maps individual, concept, and role variables to individuals, concepts, and roles respectively. We require that substitutions respect the type of a variable, so that the result of instantiating a template is a well-formed ontology. For ℒ a language, an ℒ-substitution is one whose range is a subset of ℒ. The ℒ-evaluation of over , written eval(, , ℒ), is the set of substitutions defined as follows:
eval(, , ℒ) = { an ℒ-substitution | |= }, where is the instantiation of with . Furthermore, we define eval(∅, , ℒ) to be the set of all ℒ-substitutions.
Finally, we say that an ontology is weaker than ′ if ′ |= , and strictly weaker if the reverse does not hold. 3
In this section we define the syntax and semantics of generators and GBoxes and discuss some examples.
Definition 1. A generator is an expression of the form () → ( ), for (), ( ) templates with ⊆ . and are respectively called the body and head of , and we write () and () to denote them. Example 3. : {? ⊑ Animal} → {? ⊑ ∀hasChild.?} is a generator, with a single variable ?.
Next, we define the semantics for generators and sets of generators based on entailment to ensure that generators behave independent of the syntactic form of an ontology. In this choice we diverge from the work done on OTTR [20], as OTTR template semantics is defined syntactically.
Definition 2. Let : () → ( ) be a generator. A theory satisfies wrt. ℒ if, for every ℒ-substitution such that |= , we have |= . Example 4. Consider the generator from Example 3, and let ℒ be the language of all concept names. The theory 1 = {Turtle ⊑ Mammal, Mammal ⊑
A set of generators is called a GBox. Furthermore, we define the set () (resp. ()) as the set of all bodies (resp. heads) occurring in , i.e., they are sets of ontologies.
Definition 3. Let be a GBox, an ontology, and ℒ a language. The expansion of and in ℒ, written Exp(, , ℒ), is the smallest set of theories ′ such that (1) ′ |= , (2) ′ satisfies every ∈ w.r.t. ℒ, and (3) ′ is entailment-minimal, i.e. there is no ′′ strictly weaker than ′ satisfying (1) and (2).
We call the theories in Exp(, , ℒ) expansions. This definition corresponds to the model-theoretic Datalog semantics, with consequence rather than set inclusion. Since axioms can be rewritten to be subset-incomparable, entailment-minimality is used rather than subset minimality. For example, consider { ⊑ , ⊑ } and { ⊑ }: the second one is not a subset of the first one, but weaker than it. Example 5. Recall the generator from Example 3, and let be a GBox consisting of alone. Let = {Turtle ⊑ Mammal, Mammal ⊑ Animal}, and let ℒ be the set of all concept names. Then {Turtle ⊑ Mammal, Mammal ⊑ Animal, Turtle ⊑ ∀hasChild.Turtle, Mammal ⊑ ∀hasChild.Mammal} ∈ Exp(, , ℒ). 4
We show that the semantics defined in the previous section coincides with a fixpoint-based one, investigate the role played by the language ℒ, and investigate generators with negated templates.
Theorem 1. For every , , and ℒ, we have that any two 1, 2 ∈ Exp(, , ℒ) are logically equivalent.
Hence applying a GBox to an ontology results in a theory that is unique modulo equivalence, but not necessary finite. As a consequence, we can treat Exp(, , ℒ) as a single theory when convenient.
Our definition of Exp(, , ℒ) is strictly semantic, i.e., does not tell us how to identify any ′ ∈ Exp(, , ℒ). In order to do that, we define a 1-step expansion. Definition 4. The 1-step expansion of and in ℒ, written 1Exp(, , ℒ), is defined as follows: 1Exp(, , ℒ) = ∪
{ | ∈ eval(, , ℒ)}.
⋃︁ →∈
In other words, we add to all instantiated heads of all generators applicable in . Of course, this extension may result in other generators with other substitutions becoming applicable, and so on recursively.
Lemma 1. If 1 ⊆ 2, then 1Exp(, 1, ℒ) ⊆ 1Exp(, 2, ℒ).
Definition 5. The -step expansion of and in ℒ, written 1Exp(, , ℒ), is defined as follows: 1Exp(, , ℒ) = 1Exp(. . . 1Exp( , , ℒ) . . . ).
⏟ tim⏞es We use 1Exp* (, , ℒ) to denote the least fixpoint of 1Exp(, , ℒ). Theorem 2. For finite ℒ, the least fixpoint 1Exp* (, , ℒ) exists and belongs to Exp(, , ℒ).
In other words, our fully semantic definition of Exp(, , ℒ) coincides with the operational semantics based on the fixpoint computation.
Size of the fixpoint For a generator with variables , there are at most |ℒ|| | different ℒ-substitutions. The size of the fixpoint is therefore bounded by ||×|ℒ| , where is the maximum number of variables in any ∈ . In the worst case we need to perform entailment checks for all of them, adding one instantiation at a time to . Hence determining 1Exp* (, , ℒ) involves up to (|| × |ℒ| )2 entailment checks. For finite ℒ and provided we have a fixed upper bound for , determining 1Exp* (, , ℒ) involves a polynomial number of entailment tests and results in a 1Exp* (, , ℒ) whose size is polynomial in the size of and ℒ . Finite vs infinite L The next examples illustrate the difficulties an infinite language ℒ can cause. The first example shows how an infinite ℒ can lead to infinite expansions.
Example 6. Consider the ontology = {A ⊑ ∃R.B}, the generator : {? ⊑ ∃R.? } → {? ⊑ ∃R.∃R.? }, and ℒ the set of all ℰℒ-concept expressions. Clearly, 1Exp* (, , ℒ) is infinite, and so is each expansion in Exp(, , ℒ).
The next example shows that this does not necessarily happen.
Example 7. Consider the ontology = {∃R.A ⊑ A}, the generator : {∃R.? ⊑ ?} → {∃R.∃R.? ⊑ ∃R.?}, and ℒ the set of all ℰℒ-concept expressions. Clearly, 1Exp* (, , ℒ) is infinite, but there is a finite (and equivalent) ontology to this fixpoint in Exp(, , ℒ), namely itself.
While having to explicitly specify ℒ may seem to be cumbersome, it is not very restrictive. In fact, it is easy to show that, for finite languages, generators can be rewritten to account for concepts, roles, or individuals that are missing from a given language by grounding the generators.
Definition 6. Let : → be a generator, and ℒ a finite language. The ℒgrounding of is the finite set of generators { → | an ℒ-substitution}.
Using ℒ-grounding, we can compensate for a smaller language ℒ1 ( ℒ2 by ℒ2 ∖ ℒ1-grounding generators, thereby proving the following theorem. Theorem 3. Let ℒ1 ⊆ ℒ 2 be finite languages. For every GBox there exists a Gbox ′ such that, for every , 1, 2 we have that 1 ∈ Exp(′, , ℒ1) and 2 ∈ Exp(, , ℒ2) implies 1 ≡ 2.
Of course, grounding all the generators is a very wasteful way of accounting for a less expressive language. A more clever rewriting algorithm should be possible: for example, if we allow binary conjunctions of names in ℒ2 but not in ℒ1, we can add copies of each generator where we replace variables ? with ?1⊓?2. 4.1
GBox containment and equivalence Having defined GBoxes, we now define a suitable notion for containment and equivalence of GBoxes.
Definition 7 ( ℒ-containment). Let 1 and 2 be GBoxes, and ℒ a language. 1 is ℒ-contained in 2 (written 1 ⪯ ℒ 2) if Exp(2, , ℒ) |= Exp(1, , ℒ) for every ontology .
The following lemma relating the entailment of theories and the entailment of expansions holds as a direct consequence of the monotonicty of description logics. Lemma 2. Let be a GBox, , ′ two theories and ℒ a language. If |= ′ then Exp(, , ℒ) |= Exp(, ′, ℒ).
Furthermore, the following is a rather straightforward consequence of the definition of the semantics of generators.
Lemma 3. Let be a theory, a GBox, an ontology, and ℒ a language. If |= and satisfies every generator ∈ then |= Exp(, , ℒ).
Using Lemmas 2 and 3, ℒ-containment can be shown to be decidable, and in fact efficiently so, using a standard freeze technique from database theory. Theorem 4. Let 1 and 2 be GBoxes, and ℒ a language. 1 is ℒ-contained in 2 if and only if Exp(2, , ℒ) |= for every → ∈ 1.
It follows that ℒ-containment is decidable for arbitrary ℒ (even infinite), since we can restrict ourselves to the language of all subexpressions of (1). Furthermore, the complexity is the same as that of computing an expansion of a GBox. In this section we introduce negation-as-failure to GBoxes. We extend the definition of the expansions defined in Section 3, define suitable notions of semipositive GBoxes and semantics for stratified GBoxes, and prove the corresponding uniqueness results.
To do so, a generator is now a rule of the form + (1), not − (2) → (3), for + (1), − (2), (3) templates with 3 ⊆ 1 ∪2. For the sake of notational simplicity, we restrict ourselves here to generators with at most one template in the negative body. It is worth noting, however, that all definitions and results in this section are immediately transferable to generators with multiple templates in the negative bodies (multiple templates in the positive body can of course be simply merged into a single template).
The following definition, together with Definition 3 of Exp(, , ℒ), provides a minimal model semantics for GBoxes with negation: Definition 8. A theory satisfies a generator : + (1), not − (2) → (3) wrt. ℒ if, for every ∈ eval(+ , , ℒ) ∖ eval( − , , ℒ) we have |= .
Unsurprisingly, adding negation results in the loss of uniqueness of the expansion Exp(, , ℒ) (cf. Theorem 1), as illustrated by the following example. Example 8. Let ℒ = {A, B, C, s}, = {A(s)} and = {A(?), not B(?) → C(?)}. Then Exp(, , ℒ) contains the two non-equivalent expansions {A(s), B(s)} and {A(s), C(s)}.
Next, we extend the definition of the 1-step expansion operator from Definition 4 to support negation. However, as Example 9 will show, a fixpoint does not always correspond to an expansion in Exp(, , ℒ).
Definition 9. The 1-step expansion of and in ℒ of a GBox with negation, written 1Exp− (, , ℒ), is defined as follows: 1Exp− (, , ℒ) = ∪
{ | ∈ eval(+ , , ℒ)∖eval( − , , ℒ)}.
⋃︁ + ,not − → ∈ Example 9. Consider the ontology = {Single ⊑ Person, Spouse ⊑ Person, Single ⊑ ¬Spouse, Person(Maggy)} and the following GBox = { {Person(?)}, not{Single(?)} → {Spouse(?)},
{Person(?)}, not{Spouse(?)} → {Single(?)}} The expansion Exp(, , ℒ) contains the two non-equivalent ontologies ∪ {Single(Maggy)} and ∪ {Spouse(Maggy)}. Furthermore, the iterated fixpoint (1Exp− )* (, , ℒ) is ∪ {Single(Maggy), Spouse(Maggy)}; this is, however, not an ontology in Exp(, , ℒ) as it is not entailment-minimal.
A natural question arising is whether we can identify or even characterize GBoxes with negation that have a unique expansion. To this end, we define suitable notions of semi-positive GBoxes and stratified negation. These are based on the notion of multiple templates affecting others, as formalized next. Definition 10. Let ℒ be a language, = {1, . . . , } a set of templates, an ontology, and a template. We say that activates with respect to and ℒ if there exist ℒ-substitutions 1, . . . such that ∪ ⋃︀ |= for some ℒ-substitution . For brevity we omit and ℒ if they are clear from the context. In contrast to standard Datalog with negation, the entailment of a template in the body of a generator is not solely dependent on a single generator with a corresponding head firing. Instead, multiple generators might need to fire and interact with in order to entail a body template. Hence we use the set of templates in the definition of activation.
Example 10. Consider the GBox containing generators 1 : 1(?) → {? ⊑ A}, 2 : 2(? ) → {? ⊑ B} and 3 : not{? ⊑ A ⊓ B} → 3(?). Then (1) and (2) activate {? ⊑ A ⊓ B} with respect to any and ℒ, indicating that the firing of 3 depends on the combined firing of 1 and 2.
Activation can then be used to define a notion of semi-positive GBoxes, which is analogous to semi-positive Datalog programs.
Definition 11 (Semi-positive GBoxes). Let be a GBox with negation, ℒ a language, and an ontology. is called semi-positive w.r.t. and ℒ if no negative body template − of a generator ∈ is activated by ().
As seen in example 8, even semi-positive GBoxes result in multiple nonequivalent expansions. In that example, neither the ontology nor any possible firing of can yield (). As such, we wish to restrict the theories in Exp(, , ℒ) to containing only facts derivable from and . To that end, the following definition suitably restricts the entailment of expansions.
Definition 12. Let be a GBox, an ontology, and ℒ a finite language. We say that an expansion ′ ∈ Exp(, , ℒ) is justifiable w.r.t. (, , ℒ) if the following holds: if ′ |= for some template and substitution , then |= or () activates with respect to and ℒ. We write simply ′ is justifiable when , , and ℒ are clear from the context.
Using this notion, we can show that, indeed,a GBox being semi-positive implies that its semantics is unambiguous when restricted to justifiable expansions. Theorem 5. Let be a semi-positive GBox, an ontology, and ℒ a finite language. Then the fixpoint (1Exp− )* (, , ℒ) exists, is the unique fixpoint of 1Exp− , and is contained in Exp(, , ℒ).
Corollary 1. Let be a semi-positive GBox, and ontology and ℒ a finite language. All justifiable ontologies in Exp(, , ℒ) are logically equivalent.
For a GBox to be semi-positive is a very strong requirement. Next, we introduce the notion of a stratified GBox: this does not ensure that all expansions are equivalent, but it ensures that we can determine one of its expansions by expanding strata in the right order. Again, we use () to denote the set of templates in heads of generators in , and () for the set of templates in (positive or negative) bodies of generators in .
Definition 13 (Stratification). Let ℒ be a language and an ontology. A GBox is stratifiable w.r.t. and ℒ if there exists a function : () ∪ () → N such that, for every generator + , not − → ∈ the following holds: 1. ( ) ≥ (+ ), 2. ( ) > ( − ), 3. for every ⊆ -minimal 1 ⊆ () that activates + , (+ ) ≥ ′∈1 max (′), 4. for every ⊆ -minimal 2 ⊆ () that activates − , ( − ) > max (′). ′∈2
The first two conditions in the previous definition are analogous to stratified Datalog, which intuitively states that a body literal must be evaluated (strictly, in the case of negative literals) before head literals. The second two conditions tailor the stratification to generators: generators allow for more interaction amongst their components. As opposed to Datalog, multiple heads combined might be needed to entail a body template. Thus, a body template must be defined in a higher stratum than any possible set of templates that could entail it.
Following this definition, a stratification of a GBox w.r.t. an ontology gives rise to a partition 1, . . . of , where each generator : + , not − → ( ). is in the stratum
For a GBox , an ontology and a language ℒ, we can define the precedence graph ,,ℒ as follows: nodes are the templates occuring in and 1. if + , not − → is in , then ,,ℒ contains the positive edge (+ , ) and the negative edge ( − , ); 2. for a template that occurs in the positive (resp. negative) body of a generator and any ⊆ -minimal set {1, . . . , } ⊆ () that activates w.r.t. and ℒ, ,,ℒ contains the positive (resp. negative) edges (, ) for 1 ≤ ≤ . We then get the following classification of stratified GBoxes, the proof of which is entirely analogous to the Datalog case.
Proposition 1. Let ℒ be a language and an ontology. A GBox is stratifiable w.r.t. and ℒ if its precedence graph ,,ℒ has no cycle with a negative edge. Given such a stratification, we can thus define a semantics for stratified negation. Definition 14 (Stratified semantics). Let be an ontology, ℒ a language, and a GBox stratifiable w.r.t. and ℒ. For a stratification of and the induced partition 1, . . . , of , we define strat(, , ℒ) as follows: 1. 1 = , 2. = 1Exp* (− 1, − 1, ℒ) for 1 < ≤ ,
strat(, , ℒ) = . 3. Theorem 6. Let be an ontology, ℒ a finite language, and be a GBox stratifiable w.r.t. and ℒ. Then strat(, , ℒ) exists, is independent of the choice of , and contained in Exp(, , ℒ).
When combining rules with DL ontologies, the focus has thus far primarily been on (1) encoding ontology axioms in rules for efficient query answering and (2) expanding the expressivity of ontologies using rules. In contrast, GBoxes are designed as a tool for ontology specification by describing instantiation dependencies between templates.
Datalog± [
dl-programs [
Tawny-OWL4 and the Ontology Pre-Processing Language5 (OPPL)
are formalism for manipulating OWL ontologies [
Another question is whether metamodeling in DL, in particular the encoding
scheme from [
Ontology Design Patterns (ODPs) have been proposed to capture best
practices for developing ontologies [
Reasonable Ontology Templates6 (OTTR) [
The Generalized Distributed Ontology, Modelling and Specification
Language (GDOL) [
We have presented first results about a template-based language for capturing recurring ontology patterns and using these to specify larger ontologies. Here, we list some areas that we would like to investigate in the future.
Finite representability In general, the semantics of GBoxes is such that the expansion of a GBox and ontology can be infinite if the substitution range given by ℒ is infinite. A natural question arising is whether/which other mechanisms can ensure that some expansion is finite, and how can we compute such a finite expansion? Furthermore, given , , ℒ, when can we decide whether an ontology in Exp(, , ℒ) is finite? Controlling substitutions So far, we have only considered entailment for generators when determining matching substitutions. Consider the ontology = {A ⊑ B, B ⊑ C} and the template ? ⊑ . The resulting substitutions include concepts A and B, but also a multitude of possibly unwanted, redundant concepts, e.g., {A ⊓ A, A ⊓ B, . . .}. Hence restricting substitutions to “reasonable” or possible “parametrizable” (e.g., maximally general) ones is part of future work. Entailment problems for ontologies with Gboxes The expansion of a Gbox over an ontology is itself an ontology and can be used as such for standard reasoning tasks. A question of interest is whether/how reasoning on the input ontology and GBox directly, without computing an expansion, can improve reasoning efficiency.
Furthermore, there are plenty of reasoning tasks about GBoxes which naturally reduce to reasoning tasks over ontologies. For example, checking whether a single generator : → always leads to inconsistency is equivalent to checking whether ∪ is inconsistent. This generalizes to similar questions over entire GBoxes: To check whether there exists an ontology such that every generator in a GBox fires, it suffices to check that the union of the generators’ bodies is consistent.
However, there are also global properties of Gboxes that do not reduce to individual templates. For example, do two GBoxes 1 and 2 specify equivalent ontologies? While Section 4.1 contains some results about such problems, we believe there is more to do here.
Extensions to generators Another area of future work is motivated by our
preliminary analysis of logical ontology design patterns [
For GBoxes to be indeed intention revealing, we will also support named generators and named sets of axioms in the body or the head of generators, as in OTTR [20]. 18. Eleni Mikroyannidi, Manuel Quesada-Martínez, Dmitry Tsarkov, Jesualdo Tomás Fernández-Breis, Robert Stevens, and Ignazio Palmisano. A quality assurance workflow for ontologies based on semantic regularities. In EKAW, volume 8876 of Lecture Notes in Computer Science, pages 288–303. Springer, 2014. 19. Boris Motik, Ulrike Sattler, and Rudi Studer. Query answering for owl-dl with rules.
Web Semantics: Science, Services and Agents on the World Wide Web, 3(1):41 – 60, 2005. Rules Systems. 20. Martin G. Skjaeveland, Daniel P. Lupp, Leif Harald Karlsen, and Henrik Forssell.
Practical ontology pattern instantiation, discovery, and maintanence with reasonable ontology templates. Accepted for ISWC 2018 research track, 2018.