Tractable Diversity: Scalable Multiperspective Ontology Management via Standpoint EL

1 Introduction

In many subfields of artificial intelligence, ontologies are used to provide a formal representation of a shared vocabulary, give meaning to its terms, and describe the relations between them. To this end, one of the most prominent and successful class of logic-based knowledge representation formalisms are description logics (DLs) [Baader et al., 2017; Rudolph, 2011], which provide the formal basis for the most recent version of the Web Ontology Language OWL 2 [Bao et al., 2009].

Among the most prominent families of DLs used today is EL [Baader et al., 2005], which is the formal basis of OWL 2 EL [Motik et al., 2009a], a popular tractable profile of OWL 2. One of the main appeals of EL is that basic reasoning tasks can be performed in polynomial time with respect to the size of the ontology, enabling reasoning-supported creation and maintenance of very large ontologies. An example of this is the healthcare ontology SNOMED CT [Donnelly, 2006], with worldwide adoption and a broad user base comprising clinicians, patients, and researchers among others.

However, when modelling comprehensive ontologies like SNOMED CT, one is usually facing issues related to context or perspective-dependent knowledge as well as ambiguity of language [Schulz et al., 2017]. For instance, the concept Tumour might denote a process or a piece of tissue; Allergy may denote an allergic reaction or just an allergic disposition.

In a similar vein, the decentralised nature of the Semantic Web has led to the generation of various ontologies of overlapping knowledge that inevitably reflect different points of view. For instance, an initiative has attempted to integrate the FMA1140 (Foundational Model of Anatomy), SNOMEDCT, and the NCIt (National Cancer Institute Thesaurus) into a single combined version called LargeBio and reported ensuing challenges [Osman et al., 2021]. In this context, frameworks supporting the integrated representation of multiple perspectives seem preferable to recording the distinct views in a detached way, but also to entirely merging them at the risk of causing inconsistencies or unintended consequences.

To this end, Gómez Álvarez and Rudolph [2021] proposed standpoint logic, a formalism inspired by the theory of supervaluationism [Fine, 1975]

allows for the simultaneous representation of multiple, potentially contradictory, viewpoints in a unified way and the establishment of alignments between them. This is achieved by extending the base language with labelled modal operators, where propositions □Sϕ and ♢Sϕ express information relative to the standpoint S and read, respectively: "according to S, it is unequivocal/conceivable that ϕ". Semantically, standpoints are represented by sets of precisifications, 1 such that □Sϕ and ♢Sϕ hold if ϕ is true in all/some of the precisifications associated with S. Consider the following example.

Example 1 (Tumour Disambiguation). Two derivatives of the SNOMED CT ontology (SN) model tumours differently. According to TP, a Tumour is a process by which abnormal or damaged cells grow and multiply (1), yet according to TT, a Tumour is a lump of tissue (2).

Both interpretations inherit the axioms of the original SNOMED CT (3) and are such that: if according to SN something is arguably both a Tumour and a Tissue, then it (unequivocally) is a Tumour according to TT (4). The respective assertion is made for TP (5). But Tissue and Process are disjoint categories according to SN (6).

1 Precisifications are analogous to the worlds of modal-logic frameworks with possible-worlds semantics.

While clearly incompatible, both perspectives are semantically close and we can establish relations between them. For instance, we might assert that something is unequivocally the product of a Tumour (process) according to TP if and only if it is arguably a Tumour (tissue) according to TT (7). Also, we may specify a subsumption between the classes of unequivocal instances of Tissue according to TT and to TP (8).

When recording clinical findings, clinicians may use ambiguous language, so an automated knowledge extraction service may obtain the following from text and annotated scans:

The logical statements (1)-(10), which formalise Example 1 by means of a standpoint-enhanced EL description logic, are not inconsistent, so all axioms can be jointly represented. Let us now illustrate the use of standpoint logic for reasoning with and across individual perspectives.

Example 2 (Continued fromExample 1). In this case, we can disambiguate the information given by Axiom (10) using Axiom (3) and Axiom (4), which entail that according to TT, b is unequivocally a tumour, □TTTumour(b), and with Axiom (2) also a tissue, □TTTissue(b). Moreover, we can use the "bridges" to switch to another perspective. From Axiom (8), it is clear that according to TP, b is also a tissue, □TPTissue(b), and from Axiom (7) b is the product of a tumour, □TP∃ProductOf.Tumour(b). Then Axiom (1) yields

The statement □SN[Tumour ⊓ Process](d), in contrast, will trigger an inconsistency thanks to Axiom (6), which prevents the evaluation of Tumour simultaneously as a Tissue and a Process and Axiom (2), which states that according to some interpretations, a Tumour is a Tissue. Finally, a user (e.g. a specific clinic, CL) may inherit the SNOMED CT (CL ⪯ SN) and establish further axioms, e.g.

to identify patients with cancer risk. Here, Axiom (9) lets us infer that □CL∃AssociatedWith.ColonCancerRisk(p). ❑

The need of handling multiple perspectives in the Semantic Web has led to several (non-modal) logic-based proposals. The closest regarding goals are multi-viewpoint ontologies [Hemam and Boufaïda, 2011; Hemam, 2018], which model the intuition of viewpoints in a tailored extension of OWL for which no complexity bounds are given. Similar problems are also addressed in the more extensive work on contextuality (e.g. C-OWL and Distributed ontologies [Bouquet et al., 2003; Borgida and Serafini, 2003] and the Contextualised Knowledge Repository (CKR) [Serafini and Homola, 2012]). These frameworks focus on contextual and distributed reasoning and range between different levels of expressivity for modelling the structure of contexts and the bridges between them. In the context of scalable reasoning, one should highlight the implementations that provide support for OWL2-RL based CKR defeasible reasoning [Bozzato et al., 2018].

As for modal logics, their suitability to model perspectives and contexts in a natural way is obvious [Klarman and Gutiérrez-Basulto, 2013; Gómez Álvarez and Rudolph, 2021], they are well-known in the community and their semantics is well-understood. Yet, the interplay between DL constructs and modalities is often not well-behaved and can easily endanger the decidability of reasoning tasks or increase their complexity [Baader and Ohlbach, 1995; Mosurovi´c, 1999; Wolter and Zakharyaschev, 1999]. Notable examples are NEXPTIME-completeness of the multi-modal description logic KALC [Lutz et al., 2002] and 2EXPTIMEcompleteness of ALCALC [Klarman and Gutiérrez-Basulto, 2013], a modal contextual logic framework in the style proposed by McCarthy [McCarthy and Buvac, 1998].

In this work, we focus on the framework of standpoint logics [Gómez Álvarez and Rudolph, 2021], which are modal logics, too, but come with a simplified Kripke semantics. Recently, Gómez Álvarez et al. [2022] introduced First-Order Standpoint Logic (FOSL) and showed favourable complexity results for its sentential fragments, 2 which disallowmodal operators being applied to formulas with free variables. In particular, adding sentential standpoints does not increase the complexity for fragments that are NP-hard. Yet, a finegrained terminological alignment between different perspectives requires concepts preceded by modal operators, as in Axiom (7), leading to non-sentential fragments of FOSL.

Our paper is structured as follows. After introducing the syntax and semantics of Standpoint EL (SEL) and a suitable normal form (Section 2), we establish our main result: satisfiability checking in SEL is PTIME-complete. We show this by providing a worst-case optimal tableau-based algorithm (Section 3) that takes inspiration from the quasi-model based methods [Wolter and Zakharyaschev, 1998] as used for KALC [Lutz et al., 2002], but differs in its specifics. Our approach builds a quasi-model from a graph of (quasi) domain elements, which are annotated with various constraints, to then reconstruct the worlds or, in our case, precisifications. We also show that introducing additional features such as empty standpoints, rigid roles, and nominals make standard reasoning tasks intractable (Section 4). In Section 5, we conclude the paper with a discussion of future work, including efficient approaches for reasoner implementations. Altogether, this paper provides a clear pathway for making scalable multiperspective ontology management possible.

An extended version of the paper with proofs of all results is available at https://arxiv.org/abs/2302.13187.

2 This includes the sentential standpoint variant of the expressive DL SROIQbs, a logical basis of OWL 2 DL [Motik et al., 2009b].

2 Syntax, Semantics, and Normalisation

We now introduce syntax and semantics of Standpoint EL (referred to as SEL) and propose a normal form that is useful for subsequent algorithmic considerations.

2.1 Syntax

A Standpoint DL vocabulary is a traditional DL vocabulary consisting of sets NC of concept names, NR of role names, and NI of individual names, extended it by an additional set NS of standpoint names with ∗ ∈ NS. A standpoint operator is of the form ♢s ("diamond") or □s ("box") with s ∈ NS; we use ⊙s to refer to either. A concept term is defined via

where A ∈ NC and R ∈ NR. A general concept inclusion (GCI) is of the form ⊙s[C ⊑ D], where C and D are concept terms. 3 A concept assertion is of of the form ⊙s[C(a)] while a role assertion is of the form ⊙s[R(a, b)], where a, b ∈ NI, C is a concept term, and R ∈ NR. A sharpening statement is of the form s ⪯ s′ where s, s′ ∈ NS.

A SEL knowledge base is a tuple K = ⟨S, T , A⟩, where T is a set of GCIs, called TBox; A is a set of (concept or role) assertions, called ABox; and S is a set of sharpening statements, called SBox. We refer to arbitrary statements from K as axioms. Since the axiom types in S, T , and A are syntactically well-distinguished, we sometimes identify K as S ∪ T ∪A. Note that all axioms except sharpening statements are preceded by modal operators ("modalised" for short). In case the preceding operator happens to be □∗, we may omit it.

2.2 Semantics

The semantics of SEL is defined via standpoint structures. For a Standpoint DL vocabulary ⟨NC, NR, NI, NS⟩, a description logic standpoint structure is a tuple D = ⟨∆, Π, σ, γ⟩ where:

• ∆ is a non-empty set, the domain of D;
• Π is a set, called the precisifications of D;
• σ is a function mapping each standpoint name to a nonempty subset of Π; 4
• γ is a function mapping each precisification from Π to an "ordinary" DL interpretation I = ⟨∆, ·I ⟩ over the domain ∆, where the interpretation function ·I maps:
• each concept name A ∈ NC to a set AI ⊆ ∆,
• each role name R∈NR to a binary relation RI ⊆∆×∆,
• each individual name a ∈ NI to an element aI ∈ ∆,

and we require aγ(π) = aγ(π′ ) for all π, π′ ∈ Π and a ∈ NI. Note that by this definition, individual names (also referred to as constants) are interpreted rigidly, i.e., each individual name a is assigned the same aγ(π) ∈ ∆ across all precisifications π ∈ Π. We will refer to this uniform aγ(π) by aD .

For each π ∈ Π, the interpretation function ·I for I = γ(π) is extended to concept terms via structural induction as follows:

3 The square brackets [. . .] indicate the scope of the modality, as the same modalities may be used inside concept terms.

4 As shown in Section 4, allowing for "empty standpoints" immediately incurs intractability, even for an otherwise empty vocabulary.

We observe that modalised concepts ⊙sC are interpreted uniformly across all precisifications π ∈ Π, which allows us to denote their extensions with (⊙sC)D .

A DL standpoint structure D satisfies a sharpening statement s ⪯ s′ , written as D |= s ⪯ s′ , iff σ(s) ⊆ σ(s′ ). For the other axiom types, satisfaction by D is defined as follows:

D |= ♢s[R(a,b)]

:⇐⇒ ⟨aD, bD⟩ ∈ ⋃π∈σ(s) Rγ(π)

As usual, D is a model of S iff it satisfies every sharpening

statement in S; it is a model of T iff it satisfies every GCI

τ ∈ T ; it is a model of A iff it satisfies every assertion α ∈ A;

it is a model of K = ⟨S, T ,A⟩ (written D |= K) iff it is a

model of S and a model of T and a model of A. Figure 1

illustrates a model of Example 1.

Π

Δ

Our investigations regarding reasoning in SEL will focus on standpoint versions of the well-known standard reasoning tasks, and we will make use of variations of established techniques to (directly or indirectly) reduce all of them to the first.

Knowledge base satisfiability: Given a knowledge base K, is there a DL standpoint structure D such that D |= K?

Axiom entailment: Given K and some SBox, TBox, or ABox axiom ϕ, does K |= ϕ hold, that is, is it the case that for every model D of K we have D |= ϕ?

To show that axiom entailment can be polynomially reduced to knowledge base unsatisfiability, we exhibit for every axiom type ϕ a knowledge base K¬ϕ such that K |= ϕ coincides with unsatisfiability of K ∪ K¬ϕ.

Therein, □sd := ♢s and ♢sd := □s are modality duals, and ˜ A, ˜B denote fresh concept names and ˜R a fresh role name. Concept satisfiability (w.r.t. K): Given K and a modalised concept term C, is there a model D of K with C D ̸= ∅? This task can be solved by checking the axiom entailment K |= □∗[C ⊑ ⊥]. If the entailment holds, then C is unsatisfiable w.r.t. K, otherwise it is satisfiable.

Instance retrieval: Given K and a modalised concept term C, obtain all a ∈ NI with aD ∈ C D for every model D of K. This task can be solved by checking, for all individuals a, if the entailment K |= □∗[C(a)] holds and returning all such a.

2.3 Normalisation

Before we can describe a PTIME algorithm for checking satisfiability of SEL KBs, we define an appropriate normal form.

Definition 1 (Normal Form of SEL Knowledge Bases). A

TBox T is in normal form iff, for all its GCIs □s[C ⊑ D],

1. C is of the form A, ∃R.A or A⊓A′ with A,A′ ∈ NC ∪ {⊤},
2. D is of the form B, ∃R.B, ♢s′B or □s′B with B∈NC ∪{⊥}, and
3. at least one of C,D is fromNC ∪ {⊤,⊥};

where R ∈ NR, and s, s′ ∈ NS.

An ABox A is in normal form iff all assertions have the form □s[A(a)] or □s[R(a, b)] for a, b ∈ NI, A ∈ NC, and R ∈ NR. K = ⟨S, T , A⟩ is in normal form whenever T and A are. ❑

For a given SEL knowledge base K = ⟨S, T ,A⟩, we can compute its normal form by exhaustively applying the following transformation rules (where "rule application" means that the axiom on the left-hand side is replaced with the set of axioms on the right-hand side),

Therein, ¯ C and ¯D stand for complex concept terms not contained in NC ∪{⊤}, whereas each occurrence of A on a right-hand side denotes the introduction of a fresh concept name; likewise, v, v0, and v1 denote the introduction of a fresh standpoint name. Rule (20) is applied modulo commutativity of ⊓. Most of the transformation rules should be intuitive (for the first three, keep in mind that standpoints must be nonempty). A notable exception is Rule (22), which is crucial to remove boxes occurring with negative polarity. It draws some high-level inspiration from existing work on non-vacuous left-hand-side universal quantifiers in Horn DLs [Carral et al., 2014], yet the argument for its correctness requires a much more intricate model-theoretic construction and crucially hinges on "Hornness" of K and nonemptiness of standpoints. A careful analysis yields that the transformation has the desired semantic and computational properties.

Lemma 1. Every SEL knowledge base K can be transformed into a SEL knowledge base K′ in normal form such that

• K′ is a SEL-conservative extension of K,
• the size of K′ is at most linear in the size of K, and
• the transformation can be computed in PTIME.

While K′ being a SEL-conservative extension of K brings about various valuable properties, what matters for our purposes is that this implies equisatisfiability of K and K′ , thus we will not go into details about conservative extensions.

3 A Tableau Algorithm for Standpoint EL

We present a PTIME tableau decision algorithm for SEL. Complexity-optimal tableau algorithms have been proposed for description logics with modal operators applied to concepts and axioms such as KALC [Lutz et al., 2002], which is known to be in NEXPTIME. Our case cannot be treated in the same way, as we need to take greater care to show tractability in the end. Lutz et al. [2002] build a "quasi-model" from a tree of "quasi-worlds", which is not as easily applicable in our case, so we follow a dual approach: we will build a quasimodel from a completion graph of (quasi) domain elements, where each of the latter is associated to a constraint system with assembled information regarding one individual's specifics in each precisification. We begin with some definitions. Given a SEL knowledge base K, denote by

• STK the elements of NS occurring in K together with ∗,
• INK the set of all individual names occurring in K,
• BCK (basic concepts) the concept names used in K, plus⊤,
• CK the set of concept terms used in K (with BCK ⊆ CK),
• SFK the set of subformulas of K, consisting of all axioms of K with and without their outer standpoint modality.

A constraint for K is of the form (x : C), (x : a), (x : ϕ), or (x : s), 5 where x is a variable, C ∈ CK a concept, a ∈ INK an individual, ϕ ∈ SFK a formula, and s ∈ STK a standpoint name. Constraint systems are finite sets of constraints.

Definition 2 ((Initial) Constraint System for K). The initial constraint system for K, called SK 0 , is the set

A constraint system for K is a finite set S of constraints for K such that SK 0 ⊆ S and {x : ∗, x :⊤} ⊆ S for each x in S. For a variable x, let stS(x) = {s | (x : s) ∈ S} be the standpoint signature of x in S. ❑

Intuitively, each constraint system S produced by the algorithm corresponds to a domain element ε ∈ ∆ and each variable x in S corresponds to some precisification π.

5 For better legibility, we will sometimes omit the parentheses.

Δ

Δ

Π

Δ ε ⊤

Moreover, each constraint x : X in S encodes information of ε in π. Namely, X may be an axiom that holds in π, a standpoint that contains π, or a concept expression of which ε is an instance in π. Initialising one variable per standpoint in the initial constraint system guarantees non-empty standpoints.

A constraint system is complete iff it satisfies every local completion rule from Figure 3. Local completion rules operate on constraint systems, while global rules involve more than one constraint system and operate on completion graphs.

Definition 3 (Completion Graph). An element label is a set L of triples of the form (C, s, x), where C ∈ BCK is a con-

cept, s ⊆ STK is a set of standpoints, and x is a variable. A quasi-role for a set ∆ is a tuple ⟨ε, v, ε′ , v′ , R⟩ where v and v′ are variables, ε, ε′ ∈ ∆, and R is a role name in K.

A completion graph for K is a tuple CG = ⟨∆, S, L, R⟩, with ∆ a non-empty set of elements; S a map from ∆ into constraint systems; L a map from ∆ into element labels; and R a set of quasi-roles such that

• for all ⟨ε, v, ε′, v′,R⟩∈R, (v : s) ∈ S(ε) iff (v′ : s) ∈ S(ε′ );
• if (C, s, x)∈L(ε), then {x : C}∪{x : s | s ∈ s} ⊆ S(ε). ❑

For convenience of presentation, we use the shortcut stε(v) for stS(ε)(v) and for any CG = ⟨∆, S, L, R⟩, we will refer to all ε ∈ ∆ simply as elements of CG.

CG is said to be locally complete iff for every element ε in CG, S(ε) is complete, and we call CG globally complete iff it is locally complete and no global completion rule (see Figure 3) is applicable to CG as a whole.

Intuitively, the next definition poses some global requirements for CG to warrant its eligibility as a model-substitute.

Definition 4 (Coherence). Let CG= ⟨∆, S,L,R⟩ be a completion graph for K. CG is called coherent iff

• for each a ∈ INK there is a unique element εa ∈ ∆ such that (v : a) ∈ S(εa) for all variables v in S(εa),
• for each ε, ε′ ∈ ∆ and each variable v contained in S(ε), S(ε′ ) contains some v′ such that stε(v) = stε′(v′ ), and
• if (v : ϕ)∈S(ε) and stε(v)=stε′(v′ ), then (v′ : ϕ)∈S(ε′ ). ❑ As usual in tableaux, inconsistencies emerge as clashes.

Definition 5 (Clash). A clash is a constraint of the form (x : ⊥). A completion graph CG is said to contain a clash iff S(ε) does for some ε in CG. Constraint systems or completion graphs not containing clashes are called clash-free. ❑

3.1 The Algorithm

To decide whether a given SEL knowledge base K in normal form is satisfiable, we form the initial completion graph CGI with R = ∅ and ∆ consisting of an element ε⊤ with L(ε⊤) = ∅ and S(ε⊤) = SK 0 , and for every a ∈ INK an element εa with L(εa) = ∅ and S(εa) = SK 0 ∪ {(xs : a) | (xs : ⊤) ∈ SK 0 }.

After that, we repeatedly apply the local and global completion rules from Figure 3, where LL rules have the highest priority, followed by LC, GN, and GG rules, in that order. After each rule application, we check if CG contains a clash and terminate with answer "unsatisfiable" should this be the case. If we arrive at a clash-free CG with no more rules applicable, the algorithm terminates and returns "satisfiable". The first table in Figure 2 illustrates the generated tableau for the SEL knowledge base K = {⊤ ⊑ ♢sC, C ⊑ ∃R.D}.

3.2 Quasi-Models and Quasi-Satisfiability

This section sketches how special structures, called (dual) quasi-models can serve as proxies for proper SEL models.

Definition 6 (Run, Quasi-model). Let CG=⟨∆, S,L,R⟩ be a completion graph. A run r in CG is a function mapping each element ε ∈ ∆ to a variable of S(ε), such that

• C1 if (r(ε) : s) ∈ S(ε), then (r(ε′ ) : s) ∈ S(ε′ ) for all ε, ε′ ∈ ∆ and s ∈ STK,
• C2 if ⟨ε, v, ε′, v′,R⟩ ∈ R and r(ε) = v, then r(ε′ ) = v′, and
• C3 if (r(ε) : ∃R.C) ∈ S(ε), there exists some ε′ ∈ ∆ with ⟨ε, r(ε), ε′, r(ε′ ), R⟩ ∈ R and (r(ε′ ) : C) ∈ S(ε′ ).

A quasi-model of K is a tuple Q= ⟨∆, S,L,R, Γ⟩ where ⟨∆, S,L,R⟩ is a globally complete, coherent and clash-free completion graph for K, and Γ a set of runs in ⟨∆, S,L,R⟩ such that for every ε ∈ ∆ and variable v in S(ε), there is a run r in Γ such that r(ε) = v. K is called quasi-satisfiable iff K has a quasi-model. ❑

In a nutshell, runs serve the purpose of lining up "compatible" variables, one from each individual constraint system, in a way that precisifications can be constructed (cf. Figure 2: in Q, a "compatible" set of runs over CG is displayed using dotted lines). With these notions in place, we can establish the desired result.

Theorem 2. A SEL knowledge base K is satisfiable iff it is quasi-satisfiable.

Local labelling (LL) rule:

• R⪯ If {x : s, x′ : s⪯s′ } ⊆ S but (x : s′ ) /∈ S, then set S := S ∪ {x : s′ }.

Local content (LC) rules:

• R⊓ If {x : C, x : D} ⊆ S, (x : C ⊓D) /∈ S and C ⊓D ∈ CK, then set S := S ∪ {x : C ⊓D}.
• R⊑ If {x : C, x : C ⊑D} ⊆ S but (x : D) /∈ S, then set S := S ∪ {x : D}.
• R□ If {x :□sΦ, x′ : s} ⊆ S but (x′ : Φ) /∈ S, then set S := S ∪ {x′ : Φ}.
• Rg If (x : G) ∈ S but (x′ : G) /∈ S, then set S := S ∪ {x′ : G}.
• Ra If {x : a, x : C(a)} ⊆ S but (x : C) /∈ S, then set S := S ∪ {x : C}.
• R♢ If (x : ♢sC) ∈ S and {x′ : s, x′ : C} ⊈ S for all x′ in S, then create a fresh variable x′ and set S := S ∪ {x′ : C, x′ : s, x′ : ∗, x′ : ⊤}.

Global non-generating (GN) rules:

• R↓ If (x : C) ∈S(ε), ⟨ε′, x′, ε, x, R⟩ ∈R, and ∃R.C ∈CK, but (x′ : ∃R.C) /∈S(ε′ ), then set S(ε′ ) := S(ε′ ) ∪ {x′ : ∃R.C}.
• Rr If {x : a, x : R(a, b)} ⊆ S(ε) and (x′ : b) ∈ S(ε′ ), but ⟨ε, x, ε′ , x, R⟩ /∈ R, then set S(ε′ ) := S(ε′ )∪{x : ⊤}∪{x : s | s ∈ stε(x)} and R := R∪ {⟨ε, x, ε′, x, R⟩}.
• Rr′ If {x : b, x : R(a, b)} ⊆ S(ε) and (x′ : a) ∈ S(ε′ ), but ⟨ε′ , x, ε, x, R⟩ /∈ R, then set S(ε′ ) := S(ε′ ) ∪ {x : ⊤} ∪ {x : s | s ∈ stε(x)} and R := R ∪ {⟨ε′ , x, ε, x, R⟩}.
• R∃′ If (x : ∃R.C) ∈ S(ε), (C, stε(x), x′ ) ∈ L(ε′ ) with ε ̸= ε′ or x = x′ , but ⟨ε, x, ε′′, x′′,R⟩ /∈ R whenever (C, stε(x), x′′ ) ∈ L(ε′′ ) and ε ̸=ε′′ or x=x′′, then set R := R ∪ {⟨ε, x, ε′ , x′ , R⟩}.

Global generating (GG) rule:

• R∃ If(x : ∃R.C) ∈ S(ε), but ⟨ε, x, ε′′, x′′, R⟩ /∈ R whenever (C, stε(x), x′′ ) ∈ L(ε′′ ) and ε ̸= ε′′ or x=x′′, then create ε′ and a fresh variable x′ , and then set L(ε′ ) := {(C, stε(x), x′ )}, S(ε′ ) :=SK 0 ∪{x′ : C, x′ :⊤}∪{x′ : s | s∈stε(x)}, R:=R∪{⟨ε, x, ε′ , x′ , R⟩}.

Figure 3: The tableau completion rules. G can be of the form a, (s ⪯ s′ ), or □sϕ. Φ may denote any element of SFK ∪ CK.

Proof. (sketch)We prove the correspondence by showing that every quasi-model gives rise to a model and vice versa. (⇐) Given a quasi-model Q = ⟨∆, S, L, R, Γ ⟩ of K, we obtain a model D = ⟨∆,Π, σ, γ⟩ by letting Π = Γ, σ(s) = {r | (r(ε) : s) ∈ S(ε)}, C γ(r) = {ε | (r(ε) : C) ∈ S(ε)} for C ∈ BCK, Rγ(r) = {(ε, ε′ ) | ⟨ε, r(ε), ε′ , r(ε′ ), R⟩ ∈ R} and aγ(r) = εa for all a ∈ INK. (cf. in Figure 2, see D and Q.) (⇒) Given a model D = ⟨∆, Π, σ, γ⟩ of K, we obtain a quasimodel Q = ⟨∆, S,L,R, Γ⟩ as follows: Let P := Π ∪ STK and for p ∈ P, let ¯ p denote some arbitrary but fixed π ∈ σ(p) if p ∈ STK, and otherwise ¯ p = p. Finally, let

3.3 Polytime Termination and Correctness

Next, we give an overview of our argument why our algorithm runs in polynomial time with respect to ∥K∥, the size of its input K. We observe that the number |∆| of domain elements of any completion graph CG constructed by our algorithm is bounded by 3 ∥K∥2 (†). We also find that the number of variables used in any single S(ε) is bounded by 2 ∥K∥2 and the number of constraints in S(ε) by 2∥K∥3 (‡). Now, the number of applications of R∃ is bounded by the number of elements in each completion graph, i.e. at most 3∥K∥2 in view of (†). Since the rules R⪯, R⊓, R⊑, R□, R♢, Rg, Ra, Rr, Rr′ and R↓ produce one or more new constraints in an element, the number of applications of such rules per element is bounded by 2 ∥K∥3 due to (‡). R∃′ can add, for each ε with (C, s, x) ∈ L(ε), at most one quasi-role from every variable in every element, thus we have at most 6∥K∥4 rule applications. The total number of rule applications is bounded by the rule applications per element multiplied by the bound on elements, together with the bound on R∃, which gives us

Theorem 3. The completion algorithm terminates after at most c ∥K∥6 steps, where c is a constant.

As every single rule application can be clearly executed in polynomial time with respect to K, we can conclude that our algorithm runs in polynomial time.

We are now ready to establish correctness of our decision algorithm, by showing its soundness and completeness. For both directions, Theorem 2 will come in handy. As usual, the soundness part of our argument is the easier one.

Theorem 4 (Soundness). If there is a globally complete, coherent and clash-free completion graph CG for a knowledge base K, then K is satisfiable.

Proof. (sketch) Given CG = ⟨∆, S,L,R⟩, let Γ consist of all runs on CG. Then we can show that Q = ⟨∆, S, L, R, Γ ⟩ constitutes a quasi-model for K, so we can conclude by Theorem 2 that K is satisfiable. ❑

Proving completeness requires significantly more work. We make use of a notion that, intuitively, formalizes the idea that a completion graph CG under development is "in sync" with a quasi-model Q of the same knowledge base, where Q can be conceived as a model-theoretic "upper bound" of CG.

Definition 7 (Q-compatibility). Let K be a SEL knowledge base and Q= ⟨∆q , Sq ,Lq ,Rq , Γ q ⟩ be a quasimodel for K. A completion graph CG= ⟨∆, S,L,R⟩ for K is called Qcompatible iff there is a left-total relation µ ⊆ ∆ × ∆q where

• for all g ∈ ∆ and ε ∈ ∆q , if both L(g) ⊆ Lq (ε) and {a | (x : a)∈S(g)}⊆{a | (v : a)∈Sq (ε)}, then (g,ε)∈µ,
• for each (g, ε) ∈ µ there is a surjective function µg,ε from the variables in Sq (ε) to the variables in S(g) such that
• (µg,ε(v) : s) ∈ S(g) implies (v : s) ∈ Sq (ε),
• (µg,ε(v) : Φ) ∈ S(g) implies (v : Φ) ∈ Sq (ε),
• if ⟨g, x, g′ , x′ ,R⟩ ∈ R then ⟨ε,y,ε′ ,y′ ,R⟩ ∈Rq for some (g, ε), (g′, ε′ ) ∈ µ with µg,ε(y)=x and µg′ ,ε′ (y′ )=x′. ❑

With this definition, we can establish two important insights:

• The tableau algorithm's initial completion graph CGI is Q-compatible for any quasimodel Q of K.
• Applications of tableau rules preserve Q-compatiblility. This entails that the completion graph maintained in the algorithm will be Q-compatible at all times, thus also upon termination. We exploit this insight to show completeness.

Theorem 5 (Completeness). If a SEL knowledge base K is satisfiable, the tableau algorithm will construct a globally complete, coherent, and clash-free completion graph for K.

Proof. If K is satisfiable then by Theorem 2, there is a quasimodel Q for K. According to Theorem 3, we can obtain a globally complete completion graph CG after polynomially many applications of the tableau rules, which, as just discussed, is Q-compatible. It must thus also be clash-free, because otherwise there were an element g and variable x, with (x : ⊥) ∈ S(g), and thus there is (g, ε) ∈ µ and µg,ε such that (µg,ε(x) : ⊥) ∈ Sq (ε), which is a contradiction because Q is a quasi-model. It is not hard to show that CG is also coherent, whence we can conclude that CG is a globally complete, coherent, and clash-free completion graph for K. ❑

Together with the well-known PTIME-hardness of the satisfiability problem in (standpoint-free) EL, we have therefore established PTIME-completeness of SEL and exhibited a worst-case optimal algorithm for it.

4 Intractable Extensions

While the shown tractability of reasoning in SEL is good news, one might ask if one could include more modelling features or relax certain side conditions and still preserve tractability. This section shows that tractability can be easily lost (at least under standard complexity-theoretic assumptions).

4.1 Empty Standpoints

While it may make sense on a philosophical level, one might wonder whether the constraint that σ(s) needs to be nonempty for every s ∈ STK has an impact on tractability. In fact, dropping this constraint, obtaining a logic S∅EL with the same syntax but modified semantics, would increase expressivity (standpoint non-emptiness could still be enforced in S∅EL by asserting ⊤ ⊑ ♢s⊤ for every s ∈ STK). However, satisfiability in S∅EL turns out to be NP-hard, even when disallowing usage of concept and role names entirely. The key insight that both ♢s⊤ and its negation □s⊥ can be expressed as S∅EL concepts gives rise to the following reduction from 3SAT: Assume an instance ϕ = ∨C1 ∧ . . . ∧ ∨Cn of 3SAT containing n clauses (i.e., disjunctions of literals) ∨Cj over the propositional variables P = {p1, . . . , pk}. We note that ϕ is equivalent to (∧C1 → false) ∧ . . . ∧ (∧Cn → false), where Cj is obtained fromCj by replacing every literal by its negated version. Let now {s1, . . . , sk} be a set of standpoint names and, for any literal ℓ over P, define

Then, ϕ is satisfiable iff the following S∅EL knowledge base is: Kϕ = {Lℓ ⊓ Lℓ′ ⊓ Lℓ′′ ⊑ ⊥ | {ℓ, ℓ′ , ℓ′′ } = Cj , 1 ≤ j ≤ n}.

4.2 Rigid Roles

SEL allows knowledge engineers to globally enforce rigidity of specific concepts through axioms of the shape A ⊑ □∗A. (This is in contrast to e.g. KnALC, where rigidity of concepts can only be expressed relative to a given formula.) In a similar manner, rigidity of roles (i.e., the interpretation of certain distinguished roles being the same throughout all precisifications) would represent a desirable modelling feature. Other modal extensions of DLs have easily been shown to even become undecidable when this feature is permitted, but as SEL uses a much simplified semantics on the modal dimension, these results do not carry over to SEL. Yet, we will show that just the presence of one distinguished rigid role ˙R causes SEL to become intractable as satisfiability turns CONP-hard. To demonstrate this, we reduce 3SAT to KB unsatisfiability. As above, assume an instance ϕ = ∨C1 ∧ . . . ∧ ∨Cn of 3SAT over propositional variables P = {p1, . . . , pk}. Then ϕ is satisfiable iff the following SEL TBox is unsatisfiable (with all axioms instantiated for 1 ≤ i ≤ k):

The intuition behind this is to construct a "decision tree" where ˙R acts as child relation and which (thanks to ˙R's rigidity) is synchronized across all precisifications. The leafs of this tree correspond to all possible truth assignments for p1, . . . , pk. Then we make sure that for every leaf, there exists a precisification, where this leaf is "selected" (indicated by the non-rigid concept S). This "selection marker" S is

propagated from children to parents, taking along information

on the truth assignments. Finally, when all the information on

the path leading to the selected node has been accumulated in

the root node, it is checked if this information corresponds to

an assignment satisfying ϕ. If so, a "global inconsistency" is

triggered. Figure 4 provides a small example.

Π

Δ

4.3 Nominal Concepts

Nominal concepts are a modelling feature widely used in ontology languages. For an individual o, the nominal concept {o} refers to the singleton set {oI }. Let ELO denote EL extended by nominal concepts. Several formalisms subsuming ELO, including OWL 2 EL, are known to allow for tractable reasoning [Baader et al., 2005; Krötzsch, 2010]. However, in the presence of standpoints, nominals prove to be detrimental for the reasoning complexity: satisfiability of SELO TBoxes using just one nominal concept {o} turns out to be EXPTIMEhard and thus definitely harder than for SEL. This can be shown by a PTIME reduction of satisfiability for Horn-ALC TBoxes (which is known to be EXPTIME-complete [Krötzsch et al., 2013]) to satisfiability of SELO TBoxes with just one standpoint (the global one) and one nominal concept {o}. To this end, recall that any Horn-ALC TBox can be normalised in PTIME to consist of only axioms of the following shapes:

where A, B, C can be concept names, ⊤, or ⊥. From a normalised Horn-ALC TBox T , we obtain the target SELO TBox T ′ by (i) declaring every original concept name as rigid via the axiom A ⊑ □∗A as well as (ii) replacing every axiom of the shape A ⊑ ∃R.B by the axiom

(introducing two fresh role names Src and Tgt), and replacing every axiom of the shape A ⊑ ∀R.B by the two axioms

introducing a (non-rigid) copy ˜ A for every original concept name A. With this polytime translation, satisfiability of the Horn-ALC TBox T and the SELO TBox T ′ coincide.

The intuition behind this is to emulate the DL-model of T by a standpoint structure where every role connection gets assigned its own precisification, wherein the nominal acts as "witness" for this connection and is linked to source and target element by dedicated roles. Then the "forward transfer"

of information by axioms of the shape A ⊑ ∀R.B can be

realized using the nominal element as "proxy" (cf. Figure 5).

Δ

o

Figure 5: Top: DL interpretation satisfying the Horn-ALC TBox T = {D⊑∃R.⊤,E⊑∃R.F,E⊑∃R.G,E⊑∀R.H}. Bottom: Corresponding standpoint structure satisfying T ′ .

5 Conclusion and FutureWork

In this paper, we introduced Standpoint EL, a new lightweight member of the emerging family of standpoint logics. We described the new modelling and reasoning capabilities it brings to large-scale ontology management and established a PTIME (and thus worst-case optimal) tableau-based decision procedure for standard reasoning tasks. We also demonstrated that certain extensions of SEL, which would be desirable from an expressivity point of view, inevitably come with a loss of tractability (sometimes under the assumption P ̸= NP).

Yet, several modelling features can be accommodated into SEL without endangering tractability. For instance, from a practical perspective, it appears very desirable and advantageous modelling-wise, if not just single axioms, but whole axiom sets (up to whole knowledge bases) could be preceded by standpoint modalities. By definition, an axiom of the type □sK can be equivalently rewritten into the axiom set {□sϕ | ϕ ∈ K}. While something alike is not immediately possible for axioms of the type ♢sK, our normalization rule for diamond-preceded axioms can be lifted and thus ♢sK can be rewritten to □s′K (and further to {□s′ϕ | ϕ ∈ K}) upon introducing a fresh standpoint name s′ and asserting s′ ⪯ s. Thus standpoint-modality-annotated knowledge bases come essentially for free in SEL. In fact, we already made tacit use of this modelling feature in Axiom 9 and Axiom 10 of our initial example.

Moreover, we are confident that, as opposed to nominal concepts, other modelling features of OWL 2 EL can be added to SEL without harming tractability. These include complex role inclusions (also called role-chain axioms) such as FindingSite◦PartOf ⊑ FindingSite, and the self-concept as in ApoptoticCell ⊑ ∃Destroys.Self.

Beyond exploring the tractability boundaries, potential next research endeavours include to investigate diverse feasible strategies for developing a SEL reasoner. Options worth pursuing toward this goal include

• to implement our tableau algorithm from scratch or by modifying existing open-source tableaux systems,
• to design a deduction calculus over normalised axioms that can be translated into a datalog program, akin to the approach of Krötzsch [2010], then utilizing a state-of-the-art datalog engine like VLog [Urbani et al., 2016], or
• to find a reduction to reasoning in standpoint-free (PTIME extensions of) EL that is supported by existing reasoners (such as ELK [Kazakov et al., 2014]).

With reasoners in place, appropriate experiments can be conducted to assess practical feasibility and scalability.

In addition to the EL family, further popular and computationally lightweight formalisms exist, such as the tractable profiles OWL 2 RL and OWL 2 QL [Motik et al., 2009a]. It would be interesting to investigate options to extend these by standpoint reasoning without sacrificing tractability. More generally, we intend to research the effect of adding standpoints to KR languages - light- or heavyweight - in terms of computational properties and expressivity as well as avenues for implementing efficient reasoners for them. Beyond the large and versatile family of description logics, a worthwhile target for these efforts would be existential rule languages.

Acknowledgements

This work was supported by funding from BMBF within project KIMEDS (grant no. GW0552B), by the European Research Council through the ERC Consolidator Grant DeciGUT (771779), and by the Federal Ministry of Education and Research of Germany and the Sächsische Staatsministerium für Wissenschaft Kultur und Tourismus through the Center of Excellence for AI research ScaDS.AI.