Ontologies and knowledge bases reflect not only domain specific knowledge, but also the individual points of view of their creators along with other contextual aspects. They may also difer in modelling design decisions, such as the choice of conceptual granularity or specific ways of axiomatising information. This semantic heterogeneity is bound to pose significant challenges whenever the interoperability of independently developed knowledge specifications is required. Example 1. Consider the integration of two ontologies of forestry LC and LU, adopting a land cover and a land use perspective respectively. LC characterises a forest as a “forest ecosystem” with a minimum area (G1) where a “ forest ecosystem” is an ecosystem with a certain ratio of tree canopy cover (G2). In contrast, LU defines a forest as a maximally connected area with “forest use” (G3). Both sources LC and LU agree that forests subsume broadleaf, needleleaf and tropical forests (G4), and they both adhere to the Basic Formal Ontology (BFO, Arp et al. 2015), an upper-level ontology stipulating that “land” and “ecosystem” are disjoint categories (G5).
1. Introduction Forest and all its subclasses (G4). As an alternative, we propose Standpoint Logic, a simple, yet versatile generic approach to extend existing KR formalisms by the capability to express domain knowledge relative to diverse, possibly conflicting standpoints.
In multimodal Standpoint logic [
In spite of its simple syntax and semantics, the language is remarkably versatile; it allows for specifying knowledge relative (a) to a standpoint, e.g. (G1), (b) to the global standpoint, denoted by * , e.g. (G3), and (c) to set-theoretic combinations of standpoints, e.g. (G4). Additional definabe constructs include ℐLC∪LU[Forest ⊑ Land], meaning that, “according to LC ∪ LU, it is indeterminate whether land subsumes forest” (with ℐs := ♢ s ¬ ∧ ♢ s ). The sharper operator ⪯ , used to establish hierarchies of standpoints, can be defined via s1 ⪯ s2 := □ s1∖s2 [⊤ ⊑ ⊥]. Intuitively, s1 ⪯ s2 expresses that standpoint s1 inherits the propositions of s2, by virtue of “s1 ⊆ s2” holding for the corresponding sets of precisifications. This is used in the example to “import” background knowledge from the upper-level ontology BFO (G5) and it can be used in the axiom * ⪯ (LC ∪ LU) to confine the interest to a given set of standpoints (each precisification must be associated with at least one of those). Natural reasoning tasks over multi-standpoint specifications include gathering unequivocal or undisputed knowledge, determining knowledge that is relative to a standpoint or a set of them, and contrasting the knowledge that can be inferred from diferent standpoints.
This extended abstract introduces the standpoint-enhanced version of the very expressive
description logic ℛℐ (cf. Section 2.2), which is tightly connected to the W3C-standardised
ontology language OWL 2 DL. Here, standpoint modalities are allowed only at the axiom level,
which – coupled with the semantics of the multi-modal standpoint logic framework – makes it
possible to establish a polytime translation from standpoint-enhanced ℛℐ into plain
ℛℐ (cf. Section 2.3). By virtue of this result, existing highly optimised OWL reasoners
can be used of the shelf to provide reasoning support for ontology languages from the OWL
family extended by standpoint modelling.
2. Sentential Standpoint- ℛℐ
Sentential Standpoint-ℛℐ (S[ℛℐ]) adds the standpoint modalities to ℛℐ at
the sentence (axiom) level. After an introduction to ℛℐ (Section 2.1), we provide the
syntax and semantics of S[ℛℐ] (Section 2.2), we state a small model property and finally we
present a satisfiability-preserving polynomial translation from S[ℛℐ] into plain ℛℐ
(Section 2.3). This provides us with tight complexity results and it paves the way towards
practical reasoning in “Standpoint-OWL”, since it allows us to use highly optimised OWL 2 DL
reasoners.
2.1. ℛℐ
ℛℐ is a gentle extension of ℛℐ [
In what follows, let I, C, and R be finite, mutually disjoint sets called individual names,
concept names and role names, respectively. R is subdivided into simple role names Rs and
non-simple role names Rns, the latter containing the universal role u and being strictly ordered
by ⋖. We briefly mention that unlike in the original definition of ℛℐ, we fix simplicity
of roles and ⋖ explicitly upfront, simplifying the presentation without restricting expressivity.
Then, let ℛs be the set of simple role expressions such that 1, 2 ::= s | s− | 1 ∪ 2 | 1 ∩ 2 |
1 ∖ 2, with s ∈ Rs, and let ℛ = ℛs ∪ Rns be the set of (arbitrary) role expressions. The order ⋖
is extended to ℛ by making all elements of ℛs ⋖-minimal. The syntax and semantics of concept
and role expressions as well as the diferent types of ℛℐ sentences (called axioms) are
defined as usual [
Given a set of standpoint symbols containing the universal standpoint * , we define the set ℰ of standpoint expressions via e1, e2 ::= s | e1 ∪ e2 | e1 ∩ e2 | e1 ∖ e2, where s ∈ . Then, the set S[ℛℐ] of Sentential Standpoint-ℛℐ sentences is defined inductively over ℰ and the set of ℛℐ axioms: • if Ax is a ℛℐ axiom then Ax ∈ S[ℛℐ], • if , ∈ S[ℛℐ] then ¬ ∈ S[ℛℐ], ∧ ∈ S[ℛℐ], and ∨ ∈ S[ℛℐ], • if ∈ S[ℛℐ] and e ∈ ℰ then □ e ∈ S[ℛℐ] and ♢ e ∈ S[ℛℐ].
In what follows, we assume that formulas are in SSNF, whereby their modal degree is at most 1.
The semantics of sentential Standpoint-ℛℐ is defined by “plugging” the semantics of ℛℐ axioms into a multi-modal semantics where precisifications replace worlds and the usual set of accessibility relations is replaced by the function . Thus, a Standpoint-ℛℐ structure M is a tuple ⟨Δ, Π, , ⟩ where (a) Δ is a non-empty set, the domain of M, (b) Π is the non-empty set of precisifications , (c) is a function mapping each standpoint symbol to a set of precisifications, with (* ) = Π, and (d) is a function mapping each precisification from Π to an ordinary ℛℐ interpretation ℐ = (Δ, · ℐ ) composed of the (shared1) domain Δ and a function · ℐ mapping individual names to elements of Δ, concept names to subsets of Δ, and role names to subsets of Δ × Δ.
Theorem 1. A sentential Standpoint-ℛℐ formula is satisfiable if it has a model with at most || precisifications.
Theorem 1 can be shown following a similar method to the propositional case [
of all individual names inside , plus, for each standpoint extensions of languages of the OWL family with of-the-shelf reasoners. To conclude this short paper, we provide a polynomial translation mapping any S[ℛℐ] sentence (w.l.o.g. in NNF) to an equisatisfiable set of ℛℐ axioms. With this, we establish the decidability and complexity of S[ℛℐ] and we expose a strategy to support Let Π|| be a set of size || (Theorem 1) and our translation’s vocabulary V[ℛℐ]() consist ∈ Π||, the following symbols: a concept name A for each A ∈ C; a simple role name s for each s ∈ Rs; non-simple role names r and r for each r ∈ ns
R ∖{u}; a simple role name s for each unnegated RIA inside ; a fresh constant name for each negated RIA inside ; and a concept name Ms for each s ∈ . The non-simple role names inherit their ordering ⋖ from Rns and we let r ⋖ r for each r ∈ Rns ∖{u}. contains the RIA r
The translation Tr() of is then a set of ℛℐ axioms defined as follows: First, Tr() ⊑ r for every r ∈ Rns∖{u
} and each ∈ Π||. Second, for every unnegated RIA inside and each ∈ Π||, Tr() contains the RIA ( ), with defined by
1∘ ...∘ ⊑ r ↦→ s ∘ 1 ∘ ...∘
⊑ r
r ∘ 1∘ ...∘ ⊑ r ↦→ r ∘ 1 ∘ ...∘ ∘ s
⊑ r
1∘ ...∘ ∘ r ⊑ r ↦→ s ∘ 1 ∘ ...∘ ∘ r
⊑ r r ∘ r ⊑ r ↦→ s ∘ r ∘ r ⊑ r , whereby the role expression is obtained from by substituting every role name s with s (except u which remains unaltered). Third and last, Tr() contains the GCI
⊤ ⊑ d ∈Π|| tr(, ) ⊓ d ∈Π|| ∀u.M*
The translation of unnegated and negated ℛℐ axioms where, by inductive definition,
tr(, Ax) = tr+(, Ax) tr(, ¬Ax) = tr− (, Ax) tr(, 1 ∧ 2) = tr(, 1) ⊓ tr(, 2)
tr+(, ) = ∀u.∃s .Self tr+(,
⊑ ) = ∀u.(¬ ⊔ ) tr+(, ()) = ∃u.(︀ {} ⊓ )︀ tr+(, (, )) = ∃u.(︀ {} ⊓ ∃ .{})︀ tr+(, =. ) = ∃u.(︀ {} ⊓ {})︀ tr(,
1 ∨ 2) = tr(, 1) ⊔ tr(, 2) tr( ,′ □ e ) = d tr( ,′ ♢ e ) = ⨆︀ ∈Π|| (¬trℰ (, e) ⊔ tr(, )) ∈Π|| (trℰ (, e) ⊓ tr(, )) tr− (, ) = ∃u.(︀ (∀r .¬{ }) ⊓ (∃1...∃.{ })
︀) tr− (,
⊑ ) = ∃u.( ⊓ ¬) tr− (, ()) = ∃u.(︀ {} ⊓ (¬) )︀ tr− (, (, )) = ∃u.(︀ {} ⊓ ∀ .¬{})︀ tr− (, =. ) = ∃u.(︀ {} ⊓ ¬{})︀
Therein, for any role expression , we let denote r if = r is a non-simple role name, and otherwise = . Moreover, denotes the concept expression that is obtained from by ifrst transforming it into negation normal form, second replacing concept names into a concept expression trℰ (, e) over the vocabulary {︀ M s | ∈ , role expressions r by r , and third replacing every ∃r for non-simple r with ∃r. Finally, trℰ implements the semantics of standpoint expressions: Each expression e ∈ ℰ is transformed ︀} thus: ∈ Π||
A with A and trℰ (, s) = ∀u.Ms trℰ (, e1 ∩ e2) = trℰ (, e1) ⊓ trℰ (, e2) trℰ (, e1 ∪ e2) = trℰ (, e1) ⊔ trℰ (, e2) trℰ (, e1 ∖ e2) = trℰ (, e1) ⊓ ¬trℰ (, e2)
With all definitions in place, we obtain the desired result, which concludes the paper. satisfiable with , is of polynomial size wrt. , and can be computed in polynomial time. Theorem 2. Given ∈ S[ℛℐ], the set Tr() is a valid ℛℐ knowledge base, is equiLucía Gómez Álvarez was supported by the Bundesministerium für Bildung und Forschung (BMBF, Federal Ministry of Education and Research) in the Center for Scalable Data Analytics and Artificial Intelligence ( ScaDS.AI). Sebastian Rudolph has received funding from the European Research Council (Grant Agreement no. 771779, DeciGUT).