A Tableaux-Based Method for Computing Least Common Subsumers for Expressive Description Logics

1 Motivation

Least Common Subsumers (LCSs) in Description Logics (DLs) have been introduced by Cohen et al.[1992] to denote the most specific concept descriptions subsuming all of the elements of a given collection of concepts.

Since its introduction, LCS has been usefully exploited in several application fields where the search for commonalities in a collection is needed, despite the complexity of its computation even for inexpressive DLs.

As motivation for our work stems from an actual need, we start recalling usefulness of LCS as witnessed by previous works. One of the best known applications of LCS is the support to ontology design( [Baader and K¨usters, 1998],[Kopena and Regli, 2003], [Ovchinnikova et al., 2007] ). In particular, Lutz et al. [2006] recently underlined the need to have LCS available also for the more expressive languages currently used in ontology design.

LCS has been also widely used in semantic-based information retrieval, for the definition of measures for concept similarity ([M¨oller et al., 1998], [Janowicz et al., 2008]).

Hacid et al. [2002] studied using LCS for defining and computing the best covering problem. Such a computation approach have been applied to semantic Web services discovery and composition [Benatallah et al., 2005] and, more recently, to the composition of learning resources [Karam et al., 2007]. Hacid et al. [2000] also employed LCS for schema extraction from semistructured data.

A further well-known application field is in inductive learning algorithms[Cohen and Hirsh, 1994].

Colucci et al. [2008] addressed the knowledge management problem of evaluating the Core Competence of a company, introducing inferences computed by exploiting LCS.

The variety of approaches recalled so far witnesses the importance of LCS computation in knowledge representation and reasoning literature, justifies the need for LCS in expressive DLs, and motivates our contribution, which introduces a novel general tableau-based calculus for computing LCS. The approach uses substitutions on concept terms containing concept variables. We present our method with reference to a DL more expressive than ALEN , namely ALEHINR+ .

The rest of the paper is organized as follows: in the next section previous computation results for LCS in different DLs are recalled, before introducing the DL used in the paper in Section 3. We then present a novel generalized definition of LCS in Section 4. Based on such definition and on the tableux rules for ALEHINR+ presented in Section 5, we propose a tableaux-based method for LCS computation in Section 6. Conclusions and future research directions close the paper.

2 Previous computation results

LCS computation has been investigated for a limited number of DLs, due to the complexity of the related problem.

Baader et al.[1999] propose to compute LCS as graph product of description trees representing EL, FLE and ALE concept descriptions.

An approach for computing LCS of cyclic ALN concept descriptions has been also proposed by Baader and K¨usters, which exploit automata-theoretic characterizations of valuerestriction sets [1998].

Brandt et al. investigated on the problem of computing LCS in the presence of DLs with transitive roles [2003]. The authors present an algorithm based on structural comparison of normal forms for computing LCS of FL+0 concept descriptions, and extend the algorithms by Baader et al. [1999] to EL+, ELH+ and FLE +. The paper does not deal with complexity results in the presence of transitive roles, but it is well-known that the complexity for LCS computation arises to exponential size even for DLs with only existential restriction, namely EL [Baader et al., 1999] and can neither be reduced by introducing TBoxes to shorten possible repetitions [Baader and Turhan, 2002].

So far, the most expressive investigated DL is ALEN, for which a double exponential time algorithm, based on structural comparison of normal forms, has been proposed [K¨usters and Molitor, 2005], and no proposal is available for ALEHIN R+ .

3 The Language ALEHINR+

To show the generality of our calculus, we choose the DL ALEHINR+, which is SHIN without constructs that introduce concept disjunction, namely, ⊔ and ¬. In languages including disjunction, the simplest LCS would be just C1⊔C2-or equivalently, ¬(¬C1⊓¬C2) with full negationmaking the LCS problem trivial.

Let Nr be a set of role names. A general role R can be either a role name P ∈ Nr, or its inverse P -. We admit a set of role axioms, formed by: (1) a role hierarchy H, which is a set of role inclusions of the form R1 ⊑ R2, and (2) a set of transitivity axioms for roles, denoted by trans(R). We denote by ⊑∗ the transitive closure of H ∪ {R- ⊑ S- | S ⊑ R ∈ H}. A role S is simple if it is not transitive, and for no R such that R ⊑∗ S, R is transitive.

In the following syntax for concepts, let A be any concept name in a set Nc of concept names, let R be a role, and S be a simple role.

We call At an atomic concept, while C simply concept. We consider (⩽R0) as an abbreviation of ∀R.⊥. We extend the inverse role constructor to general roles by letting R= P - if R = P , and R= P if R = P -. Moreover, we denote by ∼C the negation normal form of ¬C (see Baader et al. [2003] (Ch.2) for a definition).

As every DL, ALEHINR+ is equipped with a modeltheoretic semantics. We regret to skip a detailed definition for lack of space, referring the interested reader to Baader et al. [2003, Ch.2]. We denote by C ⊑ D subsumption between two concepts C and D. Strict subsumption is denoted by C ⊏ D, meaning both C ⊑ D and D ̸⊑ C. Intuitively, subsumption is interpreted as subset inclusion between the sets interpreting C and D; strict subsumption is strict subset inclusion. In the rest of the paper, we use concepts C1,C2, D and L that always belong to ALEHINR+. Moreover, we make use of the following property.

Proposition 1 For every four concepts C1, C2, D1, and D2: if C1 ⊑ D1 and C2 ⊑ D2, then C1 ⊓ C2 ⊑ D1 ⊓ D2.

As for concept axioms, we do not consider General Concept Inclusions (GCI) in this paper, since Baader et al. [2007] showed that even for the simple DL ALE LCS may not exist when GCIs interpreted with descriptive semantics are used. We could admit simple concept inclusions-e.g., acyclic definitions of concept names-but since they do not add expressivity to the language, for sake of simplicity we do not consider them.

Regarding Qualified Number Restrictions (Q), observe that (⩽0P.(∼C1⊓ ∼C2)) ≡ ∀P.(C1 ⊔ C2). Hence, qualified at-most number restrictions would implicitly introduce ⊔ in concepts-although inside quantifications-so we want to exclude them. Since in DLs the at-most restriction comes paired with the at-least restriction, we exclude them both, only for uniformity.

4 A logical definition of the LCS

In this section we denote by DL a generic Description Logic.

Definition 1 (LCS as a set) Let C1,C2 ∈ DL be two concepts. By LCS(C1,C2) we mean a set of equivalent concepts in DL, such that for every L ∈ LCS(C1,C2), (a) L is a common subsumer of C1 and C2-in formulas, C1 ⊑ L, C2 ⊑ L-and (b) there does not exist D ∈ DL such that C1 ⊑ D, C2 ⊑ D and D ⊏ L.

In order to write a second-order formula defining LCS, we need an alphabet Nx = {X0,X1,X2, . . .} of concept variables, which we can quantify over.

Theorem 1 L ∈ LCS(C1, C2) iff C1 ⊑ L, C2 ⊑ L, and the following formula is false:

where commas in (3) abbreviate conjunction. The proof is straightforward, since (3) is just a formal rewriting of (b) in Def.1. Observe that (3) does not belong to the Monadic Second-Order fragment proved decidable by Rabin [1969], since the formula X ∈ DL, if explicitly defined, would force to write a least fixpoint to logically define DL. We prefer instead to keep X ∈ DL as a constraint on the possible assignments for X, which restricts the possible substitutions for X to be defined later on. Intuitively, we are using general semantics for interpreting X [Henkin, 1950].

To introduce a more computation-oriented version of (3), we define the decoration of a concept. Intuitively, given a concept L, we put a new concept variable in conjunction with the filler of every universal and existential role quantification in L, plus one concept variable in the outermost level of L. Since we would like to have all variables consecutively numbered, starting at 0, we define the decoration in Algorithm 1 by means of a recursive procedure, plus a global counter i that keeps track of the last index used in whatever recursive call. Although maybe not mathematically elegant, we believe that Algorithm 1 presents this idea in the most intuitive way.

Definition 2 Let C be a concept in DL, and Nx be an alphabet of concept variables. We denote by CX the decoration of C, defined by Algorithm 1.

For example, if C is the concept A⊓∃P .(⩾2Q)⊓∀P .∀Q.B, then CX = X0 ⊓ ∃P .(X1 ⊓ (⩾ 2 Q)) ⊓ ∀P .(X2 ⊓ ∀Q.(X3 ⊓ B)). Note that CX is a (particular) concept term [Baader and Narendran, 2001], i.e., a concept formed according to the rules in (1) and (2), with the addition to (1) of the rule At -→ X, for every X in Nx. Our decorations are particular concept terms, in that every variable occurs only once in the term, and-by inspecting Algorithm 1-one can verify that variables are one-one with quantifications, plus the outermost Algorithm 1 (Decoration of a concept C)

input concept C ∈ ALEHINR+; var i := 0; return CX .= X0 ⊓ dec(C) function dec(C) case C is of the form atomic: return C C1 ⊓ C2: return dec(C1) ⊓ dec(C2) ∃R.C1: i := i+1; return ∃R.(Xi ⊓ dec(C1))

∀R.C1 : i := i+1; return ∀R.(Xi ⊓ dec(C1))

end function

variable. Observe that we do not count number restrictions as quantifiers, although their logical definition would contain a quantifier.

Definition 3 (Substitutions) A substitution σ is a set of pairs {Xi1 ↦→Di1 , . . . ,Xik ↦→Dik }, where indexes i1, . . . , ik are all different, and for every j = 1, . . . , k eachXij is a concept variable and each Dij is a concept term. A substitution is ground if every Dij contains no variables, i.e., Dij ∈ DL.

For a decorated concept CX, we inductively define σ(CX) as σ(Xi) = Di, σ(¬Xi) =∼Di, σ(C) = C if C is atomic, σ(C1 ⊓ C2) = σ(C1) ⊓ σ(C2), σ(∃R.C) = ∃R.σ(C), σ(∀R.C) = ∀R.σ(C).

The cardinality of a substitution is its cardinality as a set.

Let σ⊤,n denote the substitution {Xi ↦→ ⊤}i=0,...,n; since variables in decorations appear always in some conjunction, then for every concept C ∈ DL containing n quantifications, σ⊤,n(CX) ≡ C.

We also need renaming of variables, as bijective functions on the indices of variables. We denote a renaming by ρ. A variable renaming can also be applied to a substitution, ρ(σ), meaning that the index of each variable changes according to ρ; e.g., if σ = {X0 ↦→ A,X1 ↦→ B}, and ρ is the renaming {0 ↦→ 1, 1 ↦→ 2}, then ρ(σ) = {X1 ↦→A,X2 ↦→B}.

We can now reformulate Thm.1 (for DL =ALEHINR+) in a way that leads to a direct computational method.

Theorem 2 Let C1,C2,L ∈ ALEHINR+. Then L ∈ LCS(C1,C2) iff C1 ⊑ L,C2 ⊑ L, and the formula below is false:

Proof. Since Thm.1 has the same premises of Thm.2, the latter amounts to an equivalence between formulas (3) and (4), which we prove below. Let 0, . . . , n be the indexes of concept variables in LX.

(3)⇒(4) If (3) holds, then there is a concept L0 ∈ DL such that all three conditions: C1 ⊑ L0, C2 ⊑ L0, and L0 ⊏ L hold. Then let σ be the substitution {X0 ↦→ L0} ∪ {Xi ↦→ ⊤}i=1,...,n. Applying σ to LX we obtain L0 ⊓σ⊤,n(dec(L)), which is equivalent to L0 since σ⊤,n(dec(L)) ≡ L and L0 ⊏ L. Since all conditions for σ(LX) hold, the claim follows. (4)⇒(3) If (4) holds, then we use σ(LX) as a witness for ∃X in (3), proving all four conditions of (3). First condition is met because σ(LX) ∈ DL since σ is ground. Second and third conditions hold by hypothesis. Regarding fourth condition (proving σ(LX) ⊏ L), we prove subsumption separately (to ease readability) in Lemma 1 below, while fourth condition in (4) implies that subsumption holds strictly.

Lemma 1 For every given concept C ∈ ALEHINR+, and every ground substitution σ, it holds σ(CX) ⊑ C.

Proof. By induction on the structure of C. Base cases: when C is atomic (no structure), CX = X0 ⊓ C contains just one concept variable. Then σ(X0⊓C) = σ(X0)⊓C = D0⊓C ⊑ C by definition of ⊓, whatever D0, and hence for every σ.

Inductive cases: we now show that the claim holds for ∃R.C1, given that it holds for C1 which is structurally simpler. Suppose C1 has n ≥ 0 quantifiers, hence (C1)X has n+1 variables X0, . . . , Xn. Observe that by letting ρ = {i ↦→ i + 1}, it holds (∃R.C1)X = X0 ⊓ ∃R.ρ((C1)X), where the renaming is necessary because in (C1)X variables are numbered from 0. Observe that ρ is a bijection, hence its inverse ρ-1 is well defined. Then, for every substitution σ over n+2 variables, σ((∃R.C1)X) = σ(X0) ⊓ ∃R.σ(ρ((C1)X)). Let σ′ be σ without X0 ↦→ D0, and let σ1 = ρ-1 (σ′ ). Then σ(ρ((C1)X)) = σ1((C1)X), which is subsumed by C1 by inductive hypothesis. Hence ∃R.σ(ρ((C1)X)) ⊑ ∃R.C1, and the subsumption holds also if (whatever concept) D0 is conjoined on the left-hand side. Since we made no restrictions on σ, for every σ, the claim σ((∃R.C1)X) ⊑ ∃R.C1 holds. A similar proof can be laid out for ∀R.C1.

Regarding C1 ⊓ C2, the inductive hypothesis is that the claim holds for C1 and C2 separately, which are both structurally simpler. Again, suppose that both C1 and C2 have at most m, n ≥ 0 quantifiers, respectively, and let ρ be now the renaming {i ↦→ i + m}i≥1. For this renaming, (C1 ⊓ C2)X ≡ (C1)X ⊓ ρ((C2)X), where both decorations introduce a variable X0 (which ρ does not rename, since it applies to i ≥ 1), and equivalence holds since X0 ⊓ X0 ≡ X0. Then, for every σ on m+n+1 variables, σ((C1 ⊓C2)X) ≡ σ1((C1)X) ⊓ σ2((C2)X), where σ1 is just σ restricted to the first m + 1 variables, while σ2 is built as follows: let σ′ be σ restricted to the last n variables; let ρ′ = {i + m ↦→ i}i=m+1,...,n. Then, σ2 = {X0 ↦→ D0} ∪ ρ′ (σ′ ). By inductive hypothesis, both σ1((C1)X) ⊑ C1 and σ2((C2)X) ⊑ C2 hold. By Prop.1, the claim is obtained.

Observe that Thm. 2 refers to ALEHINR+ only because both Algorithm 1 and Lemma 1 refer to ALEHINR+.

5 Tableaux Rules for ALEHINR+

We first give an intuition of the way our calculus proceeds. To prove or disprove Formula (4), we expand three tableaux, one for each of the three conditions: T1 for C1 ⊑ LX, T2 for C2 ⊑ LX, and T3 for L ̸⊑ LX. The tableaux are first expanded using tableaux rules (T-rules), treating concept variables as concept names. Then, by using substitution rules (S-rules), we try to find a substitution σ satisfying (4), i.e., closing T1 and T2 and leaving T3 open. The substitution might make applicable some other T-rule, and so on, till no rule is applicable. If all branches of T1 and T2 close, and at least one branch of T3 is open, we found a substitution σ

All rules are applicable only if x is not blocked. For each i = 1, 2, 3, Li is a branch in Ti.

• ⊓-rule : if C ⊓D ∈ Li(x), then add both C and D to Li(x)
• ⊔-rule : if C ⊔D ∈ Li(x), then add either C or D to Li(x)

∃-rule : if ∃R.C ∈ Li(x), and x has no R-successor y with C ∈ Li(y), then pick up a new individual y, add R to L(x, y), and let Li(y) := {C}

• ∀-rule : if ∀R.C ∈ Li(x), and there exists an individual y such that y is an R-successor of x, then add C to Li(y).
• ∀+-rule : if ∀S.C ∈ Li(x), with trans(R) and R ⊑∗ S, there exists an individual y such that y is an R-successor of x, and ∀R.C ̸∈ Li(y), then add ∀R.C to Li(y)
• ⩾-rule : if (⩾nS) ∈ Li(x), and x has not n S-neighbors y1, . . . , yn with yℓ ̸= yj for 1 ≤ ℓ < j ≤ n, then create n new successors y1, . . . , yn of x with Li(x, yℓ) = {S}, and yℓ ̸= yj , for 1 ≤ ℓ < j ≤ n
• ⩽-rule : if (⩽nS) ∈ Li(x) with n ≥ 1, and there are more than n S-neighbors of x, and there are two S-neighbours y, z of x, y is an S-successor of x, and not y ̸= z then (1) add Li(y) to Li(z), (2) for every R ∈ Li(x, y) if z is a predecessor of x then add R- to Li(z, x) else add R to Li(x, z), (3) let Li(x, y) = ∅, and (4) for all u with u ̸= y, set u ̸= z

Figure 1: Tableaux rules (T-rules) for ALEHINR+ (rephrased from Tobies [2001, p.128])

validating (4), otherwise, we prove that no such σ exist, disproving (4). We warn the reader that the calculus we present in this section does not compute an LCS; it just tries to prove Formula (4), by exhibiting a common subsumer of C1,C2 which is "better" than L. In the next section, we use such a calculus to compute-in an incremental fashion-a finite LCS (if one exists).

Rules for constructing tableaux in ALEHINR+ (Fig. 1) are a subset of the ones for SHIQ, and have been proved [Tobies, 2001] sound and complete. We summarize them here for sake of completeness, remarking that we just inherit them from past research. Any inaccuracy is due to our rephrasing. In such rules, blocking is pair-wise blocking as defined by, e.g., Tobies [2001] (p.125); our only addition is that concept variables are treated as concept names for what regards blocking.

We recall that an individual y is an S-successor of x in Li, (for i = 1, 2, 3) if for some role R, both R ∈ Li(x, y) and R ⊑∗ S. Conversely, y is an S-predecessor of x if x is an S-successor of y. An individual y is an R-neighbor of x if either y is an R-successor of x, or x is an R--successor of y. The definitions of successor, predecessor, and neighbor allow us to treat roles and inverse roles in a uniform way, both in T-rules (Fig. 1) and in subsequent S-rules (Fig. 2).

Differently from Tobies [2001], we say that T-rules construct a branch L, while we call tableau the set of all different branches that can be constructed applying T-rules. Branches are different because of the nondeterminism present in ⊔-rule and ⩽-rule (we ignore differences due to possible renaming of new individuals in ⩾-rule). A branch L is closed if for some individual x, either (a) ⊥ ∈ L(x), or (b) {A, ¬A} ⊆

L(x) for some A ∈ Nc, or (c) (⩽nR) ∈ L(x) and there are n + 1 R-neighbors y1, . . . , yn+1 of x such that yi ̸= yj ∈ L for 1 ≤ i < j ≤ n+ 1. A branch is T-complete if no T-rule is applicable. A tableaux is closed if all its T-complete branches are closed, it is open if there exists at least one T-complete branch which is not closed.

We now give a sketchy intuition about T-rules, referring the interested reader to Baader et al. [2003, Ch.2]. A tableau for C ∈ L(a) tries to construct a model for this formula. A T-complete, open branch identifies such a model, in which individuals that are pairwise blocked (say, b) represent potentially infinitely many individuals all with the same properties ("copies" of b). A closed branch, instead, exhibits a plain contradiction, hence no model can be defined from it; so when all branches are closed, the initial formula is proved to be unsatisfiable.

We are now able to present our original part of this section, namely, substitution rules (S-rules) dealing with concept variables, in Fig. 2. There is a substitution rule for every syntax rule in (1)-(2), except conjunction. This is because substituting, say, X1 ↦→ X2 ⊓ X3, and repeatedly X2 ↦→ X4 ⊓ X5, etc., would yield infinite branching in our substitution calculus, which should be carefully dealt with by some restrictions on substitution applications. Instead, we prefer to deal with conjunctions in an incremental fashion, as explained in the next section.

Our tableaux contain concept variables; we denote by σ(T) the application of the substitution σ to every concept in every constraint of T. Since we operate on a system of three tableaux, we denote it globally as 〈T1,T2,T3〉. For such a system, σ〈T1,T2,T3〉 denotes 〈σ(T1), σ(T2), σ(T3)〉. When both a T-rule and an S-rule is applicable to 〈T1,T2,T3〉, T-rules have always precedence over S-rules.

When the application of a rule to 〈T1,T2,T3〉 yields 〈T′1 , T′2 , T′3 〉, we say that 〈T′1 , T′2 , T′3 〉 directly derives from 〈T1,T2,T3〉. Then derives is just the transitive closure of "directly derives". In what follows, we assume that T- and S-rules are applied to three tableaux that always start as follows:

For such tableaux, the following properties can be isolated.

Lemma 2 Let 〈T1,T2,T3〉 start as above. Then, (1) every concept variable occurs always with a negation in front in every constraint of every tableaux; (2) every T-complete branch Li of every Ti contains at most one concept variable X such that ¬X ∈ Li(x), for some individual x.

Proof. Property (1) can be proved by induction on T- and S-rule applications. Base: in the initial tableaux (5)-(7), concept variables appear only in ∼(LX), and since variables occur positively in LX, negation normal form puts a "¬" in front of every variable. Induction: suppose the claim holds for 〈T1,T2,T3〉. By inspection, T-rules never introduce nor delete negations in concepts, so the claim holds also after a Trule has been applied. S-rules which introduce new concept All rules are applicable only if L ∈ T1 ∪ T2, L is open, and the substitution is not σ-blocked. Rules above the separating line have precedence over rules below it.

• σ⊤-rule : if ¬X ∈ L(x), then apply σ = {X ↦→ ⊤} to 〈T1, T2, T3〉
• σN-rule : if {¬X,A} ⊆ L(x) for some A ∈ Nc, then apply σ = {X ↦→A} to 〈T1,T2,T3〉
• σ¬N-rule : if {¬X, ¬A} ∈ L(x) for some A ∈ Nc, then apply σ = {X ↦→¬A}, to 〈T1,T2,T3〉
• σ⩾-rule : if ¬X ∈ L(x) and there are exactly nR-neighbors of x, then apply σ = {X ↦→ (⩾mS)}, where m is between 0 and n, and R ⊑∗ S
• σ⩽-rule : if {¬X, (⩽nS)} ⊆ L(x), then apply σ = {X ↦→ (⩽nR)} to 〈T1, T2, T3〉, for some role R such that R ⊑∗ S .
• σ∀-rule : if {¬X, ∀S.C} ⊆ L(x), then apply σ = {X ↦→ ∀R.Y } to 〈T1,T2,T3〉, where Y denotes a concept variable not appearing in 〈T1, T2, T3〉, and R ⊑∗ S
• σ∃-rule : if {¬X, ∃R.C} ⊆ L(x), then apply σ = {X ↦→ ∃S.Y } to 〈T1,T2,T3〉, where Y denotes a concept variable not appearing in 〈T1, T2, T3〉, and R ⊑∗ S

Figure 2: Substitution rules (S-rules) for ALEHINR+

variables (σ∀ and σ∃) apply a substitution X ↦→ D (where D is either ∀R.Y or ∃S.Y ) to an existing negated variable ¬X (by induction hypothesis). By Def.3, ¬X is substituted with ∼D, so also newly introduced concept variables satisfy the claim.

We now turn to prove (2). At start, concept variables appear only in ∼(LX), and S-rules never increase the number of concept variables: all S-rules reduce by 1 the number of concept variables, but for σ∀ and σ∃ that introduce a new variable Y , but remove X. So, we can base our induction on the number n of variables of LX. If L contains no quantifications (i.e., L is a conjunction of atomic concepts), then ∼(LX) = ∼(X0 ⊓L) = ¬X0⊔ ∼L, so the claim holds for one variable X = X0 and x = a. Suppose the claim holds for concepts with n variables. If L contains n + 1 variables, then it must contain at least one quantification, and LX can be decomposed as X0 ⊓ L1, where L1 is a concept term that contains at least one quantification, so another variable, and at most n variables in total. Hence, ∼(LX) = ¬X0 ⊔ ∼(L1), so from ∼(LX) ∈ Li(a) T-rules can obtain two branches, say, L′i and L′′ i , the former with ¬X0 ∈ L′i (a), and the latter with ∼(L1) ∈ L′′ i (a). For L′i the claim holds directly, while for L′′ i it holds by inductive hypothesis since it contains n variables.

The above lemma justifies the absence of S-rules acting for constraints of the form X ∈ Li(x), since starting from 〈T1,T2,T3〉 as in (5)-(7), such constraints never appear.

A branch is S-complete if no S-rule is applicable. We call a branch complete when it is both T-complete and S-complete.

Theorem 3 (Soundness and completeness) Let C1,C2,L as in Thm.2, and let 〈T1,T2,T3〉 be defined as in (5)-(7). Then Formula (4) is true if and only if there is a way of applying S-rules, obtaining a global substitution σ, such that both σ (T1) and σ (T2) close, and σ (T3) is open.

Proof. (Only if.) Validity of Formula (4) requires a ground substitution σ′ . Now σ′ may not be used to prove directly the claim, since it may contain ⊓ in some substitution Xi ↦→Di, and ⊓ is not reconstructed by S-rules. So let σ be a substitution obtained from σ′ by choosing only one conjunct in the outermost ⊓ of each Di, and if such a conjunct contains an ⊓ (also inside quantifications), recursively choosing one conjunct, till one obtains a D′i without ⊓s; the choice is made by inspecting how T-rules build the branches of the (variablefree) tableau σ′ (T3). Observe that σ′ (∼(LX)) = σ′ (¬X0) ⊔ σ′ (∼(L1)) for a suitable concept term L1, and suppose that σ′ contains the substitution X0 ↦→ E1 ⊓ E2. Therefore, ⊔- rule applied to σ′ (∼(LX)) ∈ L3(a) yields three branches, ¬E1 ∈ L′3 (a), ¬E2 ∈ L′′ 3 (a), and σ′ (∼(L1)) ∈ L′′′ 3 (a). Since σ′ validates (4), at least one among L′3 ,L′′ 3 , L′′′ 3 can be turned by T-rules into a T-complete, open branch. If such a branch is L′3 , choose X0 ↦→ E1 for σ, if it is L′′ 3 choose E2, while if the open branch stems from L′′′ 3 then choose whatever E1,E2, indifferently. Clearly if Ei is chosen and Ei still contains conjunctions, the choice is recursively repeated. Soundness of T-rules ensures that the choice of a ⊓-free substitution σ can always be made in such a way that, finally, Trules can obtain from σ(T3) a T-complete, open branch. Observe also that σ′ (T1), σ′ (T2) must close by completeness of T-rules, that is, every branch stemming from them must close. Now branches from σ(T1) and σ(T2) are a subset of the branches from σ′ (T1), σ′ (T2), hence all of them must close too. It remains to show that σ can be reconstructed by repeated application of S-rules, and which can be proved by induction on the quantifications of each Di in Xi ↦→Di ∈ σ.

(If.) If S-rules (intertwined with T-rules) can construct a ground substitution σ such that both σ (T1) and σ (T2) close, and σ (T3) is open, then by soundness of T-rules, σ is a witness validating Formula (4).

The above theorem does not exclude that, when Formula (4) is false, the calculus runs forever. In fact, the reader could verify that in the example trans(P), C1 = ∃P ⊓ ∀P.∃P.(A ⊓ C), C2 = ∃P ⊓ ∀P.∃P.(B ⊓ C), and L = ∃P ⊓ ∀P.∃P.C T- and S-rules together run indefinitely. Intuitively, the calculus can go astray when already L ∈ LCS(C1,C2), and transitive roles keep producing new individuals and concepts that, in turn, trigger the application of an S-rule, which may add new concepts to old individuals, and such concepts can propagate to new individuals, destroying pairwise blocking. Therefore, although S-rules require some other constraints to be already present in the branch, they also need a blocking condition, to prevent their infinite application.

A substitution X ↦→ ∃R.Y is S-blocked for ¬X ∈ Li(x) in 〈T1,T2,T3〉 if 〈T1,T2,T3〉 derives from some 〈T′1 ,T′2 ,T′3 〉, in which there is some individual x′ such that: (i) ¬X′ ∈ L′i (x′ ), (ii) Li(x) = L′i (x′ ), (iii) for every Rsuccessor y of x in Li, there exists an R-successor y′ of x′ in L′i such that Li(y) = L′i (y′ ), (iv) for every S, the number of different S-neighbors of x in Li is the same as the number of different S-neighbors of x′ in L′i , and (v) the σ∃-rule has been applied to 〈T′1 ,T′2 ,T′3 〉, with the substitution X′ ↦→ ∃R.Y ′ . The S-blocking of a substitution X ↦→ ∀R.Y is defined analogously. Observe that we compare Li(x) (the concepts attached to x in 〈T1, T2, T3〉) with L′i (x′ ), that is, the concepts attached to x′ in the old state 〈T′1 ,T′2 ,T′3 〉. Also, note that Lemma 2 allows us to define blocking only for constraints of the form ¬X ∈ Li(x).

Rule σ∃ is S-blocked for ¬X ∈ Li(x) in 〈T1,T2,T3〉 if either it is simply not applicable, or every possible substitution for X allowed by σ∃ is S-blocked, and analogously for Rule σ∀. Note that if {¬X, ∃R.C} ⊆ L(x), then for each role S such that R ⊑∗ S, Rule σ∃ allows the substitution X ↦→ ∃S.Y , so S-blocking prevents all these substitutions. Finally, we say that a branch is S-blocked if it is not closed and contains a constraint ¬X ∈ Li(x) for which both Rule σ∃ and Rule σ∀ are S-blocked, and 〈T1,T2,T3〉 is Sblocked if either T1 or T2 contain an S-blocked branch.

Now we modify the completeness of a branch by saying that a branch is S-complete if no S-rule is applicable, taking also S-blocking into account. Clearly, when we stop the calculus because of S-blocking, we have to prove that no substitution was ever to be found.

Theorem 4 If 〈T1,T2,T3〉 is S-blocked, no 〈T′1 ,T′2 ,T′3 〉 such that T′1 and T′2 are closed, and T′3 is open, can be derived from it.

Proof. (Sketch) We intuitively view our calculus as a game between Player T, whose moves are T-rules, and player S, whose moves are S-rules. Faithfully to our precedences, T moves whenever she can, S moves only if T cannot move, and S should use a move above the line in Fig. 2 whenever he can. S wins if he can reach a state 〈T1, T2, T3〉 in which both T1 and T2 are closed, and T3 is open, while T wins in every other case (including infinite runs). Intuitively, S tries to build some finite proof of (4), while T responds by constructing a (possibly infinite) model that would serve as a counterexample for that proof. In this setting, the claim is proved if T has a winning strategy whenever 〈T1, T2, T3〉 is S-blocked.

In fact, suppose that in such a case S tries anyway a substitution X ↦→ D for ¬X ∈ Li(x). Then, T can respond in the same way she did in 〈T′1 ,T′2 ,T′3 〉 when S played X′ ↦→ D′ for ¬X′ ∈ L′i (x′ ). Conditions (ii)-(iv) ensure that after S plays X ↦→ D in 〈T1,T2,T3〉, T can play on x the same rules she played on x′ after S played X′ ↦→ D′ in 〈T′1 ,T′2 ,T′3 〉. S will not succeed in closing Li, otherwise by precedence of Rules σ⊤, σN, σ¬N, σ⩾, σ⩽, over Rules σ∀ and σ∃, S would have closed L′i in 〈T′1 ,T′2 ,T′3 〉 before deriving 〈T1, T2, T3〉.

Theorem 5 (Termination) Let T-rules and S-rules be applied according to blocking conditions, giving always precedence to T-rules. Then there is no infinite sequence of applications of T- and S-rules starting from 〈T1,T2,T3〉 as in (5)-(7).

Proof. (Sketch) Termination of T-rules alone was proved by Tobies [2001] (Lemma 6.35). Termination of T- and Srules together stems from S-blocking, which eventually occurs since S-rules add concepts that are in the syntactic closure of C1, C2, L and H. In fact, observe that, e.g., σ∃ substitutes X with ∃S.Y only if ∃R.C ∈ Li(x), and ∃R.C does not come from another substitution in the same branch, because of Lemma 2.

In conclusion, checking whether L ∈ LCS(C1,C2) is a decidable problem for C1, C2, L ∈ ALEHINR+ .

6 Computing the LCS

The previous section set up a calculus for the LCS decision problem. We now set an iterative algorithm that computes the LCS by repeatedly solving Formula (4) for increasingly better Ls.

Algorithm 2 Computing an LCS of C1, C2

input concepts C1, C2 var concept L := ⊤, concept L1 repeat (*) T1 := {C1 ∈ L1(a), ∼(LX) ∈ L1(a)}; T2 := {C2 ∈ L2(a), ∼(LX) ∈ L2(a)}; T3 := {L ∈ L3(a), ∼(LX) ∈ L3(a)}; apply T-rules and S-rules to 〈T1, T2, T3〉 if a substitution σ s.t. (T1, T2 close and T3 is open) is found then L1 := σ(LX); L := L1 else L1 := nil; until (L1 = nil) return L;

Termination of the above algorithm implies the existence of a finite LCS for every pair of concepts in ALEHINR+. This problem is out of the scope of this paper, hence we give a weaker termination proof.

Theorem 6 Let C1,C2 ∈ ALEHINR+. If LCS(C1,C2) contains a finite concept expression, then Algorithm 2 terminates with L ∈ LCS(C1, C2).

Proof. If there exists a finite concept ˆL ∈ LCS(C1, C2), it must have a finite number of non-redundant conjuncts. In each iteration (*), in order for T3 to be open, L1 = σ(LX) must have at least one non-redundant conjunct more than L. Hence after | ˆL| iterations, the until condition is reached.

We remark that for DLs for which a finite LCS always exists, the above theorem implies that Algorithm 2 always terminates. For instance, in ALEN there always exist a finite LCS(C1,C2), whose size is exponential in the sizes of C1,C2 [K¨usters and Molitor, 2005]. Hence for C1,C2 ∈ ALEN, Algorithm 2 iterates (*) a number of times exponential in |C1| + |C2|.

Also, we remark that if iterations (*) are stopped before the until condition is true, an invariant of (*) is that the current value of L is a common subsumer of C1,C2 (although not the least one). In this sense, Algorithm 2 is also an anytime approximation algorithm for LCS.

7 Conclusion and Perspective

Although Least Common Subsumer is one of the most interesting and usefully exploited non-standard inference service for Description Logics, its computation for expressive DLs is still an open challenge.

In this paper we formulated the problem of evaluating LCS in terms of second-order formulas where variables represent general DL concepts. Based on this formulation we also proposed a novel general tableau-based calculus to compute a solution to a LCS problem and presented the whole calculus for an expressive DL, namely ALEHINR+.

Having a calculus based on well-founded analytic tableaux surely presents many advantages both from a practical point of view and from a theoretical one. First, our approach may ease implementing the computation of LCS in state-of-the-art tableaux-based reasoners (Pellet, FaCT++, RacerPro), also exploiting well known optimization techniques for tableaux in DLs [Baader et al., 2003, Ch.9]. Secondly, the analysis of soundness and completeness for a tableau-based algorithm is less tricky than the one based on structural algorithms as the ones proposed so far for LCS. Finally, but even more important, for DLs in which a finite LCS may not always exist [Baader et al., 2007], a terminating algorithm for computing LCS cannot exist, while a sound and complete calculus can be devised along the lines we showed-analogously to sound and complete calculi for full First-Order Logic.

In perspective, our formulation and computation of LCS paves the way to further results for computing other useful non-standard reasoning services in DLs.

Acknowledgments

We thank Franz Baader for useful discussions on LCS and pointers to his relevant literature, and all reviewers for thorough revisions and suggestions. We acknowledge partial support of Apulia region Strategic Projects PS 092 and PS 121.