Although standard description logics are accurate tools to capture inferences from extensional knowledge bases, logics like ALC are unreasonably strong in intentional contexts. The successful modeling of cases in which, e.g., a knowledge base is interpreted as describing a conversational agent's beliefs or goals thus requires a more constrained notion of closure. In this paper, we identify several inferences in ALC whose validity is questionable for such applications and describe two subsystems of ALC that better fit the use-case.
The phrase “predicate calculus” denotes the “classical” first-order logic of Frege and Russell. Although various description logics correspond to distinct fragments of classical first-order logic, the semantic foundation is almost universally a classical one. As a tool to “capture facts” about the world, this Boolean framework is well-suited to many use-cases. For example, a knowledge base representing metadata about an organization’s assets will likely be interpreted extensionally, that is, the truth or falsity of an assertion make up the primary logical consideration. Thus, the classical framework is generally sound with respect to extensional contexts.
However, not all contexts about which one wishes to reason are extensional; many applications exist in which veridical considerations do not take center
Description logics like ALC and SROIQ are tools for knowledge representation,
i.e., the modeling of and reasoning about information. In their introduction to
[
Challenges for ALC in Intentional Contexts In this section, we review a number of ways in which ALC—and thus all stronger description logics—is deductively promiscuous in intentional contexts. We briefly provide a pr´ecis of the description logic ALC. Its language is built from pairwise disjoint classes of primitive individual names, concept names, and role names, natural interpretations of which are individuals (i.e., constants in first-order logic terms), classes (i.e., unary predicates), and relations (i.e., binary predicates). These terms make up expressions when closed under syncategorematic terms allow us to represent many details of a domain.
The language includes primitive top and bottom concepts ⊤ and ⊥, interpreted as a universal class and an empty class, respectively. The class of concepts is constructed by closing the primitive concepts under the following, where r is a role name:
C ::= ⊤|⊥|¬C|C ⊓ C|C ⊔ C|∃r.C|∀r.C ¬C is the complement of C and C ⊓ D, C ⊔ D are the intersection and union of C, D, respectively. We read ∃r.C as the class of individuals a that bears the relation r to some C and ∀r.C as the class of individuals a for which a bears r to only members of C. Then, where a, b are individual names, r is a role name, and C, D are concept names, sentences are formed as follows:
ϕ ::= a : C|ha, bi : r|C ⊑ D|C ≡ D In the sequel, our choice of terms will be self-documenting, where the intended interpretations should be clear. 2.1
We identify cases in which ALC appears to overgenerate, licensing consequences
too permissively for particular use-cases. That ALC is promiscuous should not be
controversial; intentional interpretations of knowledge bases are hyperintensional
in the sense of [
These concepts see implementation in OWL 2 [
Thus, the utility of a recommendation system’s suggestions with respect to a domain will be enhanced for understanding the interlocutor’s command of that domain. A clear indicator would be the breadth and degree of correctness of the interlocutor’s beliefs about that domain, which could be measured from the number and accuracy of the interlocutor’s assertions stored in an intentional knowledge base.
Example 1 A conversational agent assists the interlocutor as she navigates an online storefront devoted to classical music. After the initial interactions, the agent has recorded the following ABox A0 as reflecting the agent’s explicit beliefs about classical music: – Mahler : ∀composerOf.Symphony – hMahler, Kindertotenliederi : composerOf – Kindertotenlieder : ¬Symphony – MahlerSymphony5 : Symphony ⊓ Modernist Suppose that the agent takes the percentage of correct classifications of musical pieces within the concept Symphony as a coarse metric for the agent’s command of classical music. Given the intended interpretation of the terms, it appears that the interlocutor has correctly classified each of the two compositions mentioned in A0; intuitively, she has evidenced some expertise with respect to the domain.
Clearly, this task requires some deductive machinery; to infer the correct classification of MahlerSymphony5 requires an inference from MahlerSymphony5 : Symphony ⊓ Modernist to MahlerSymphony5 : Symphony. But the deductive machinery of ALC leads to a conflict with this intuition. The interlocutor has evidently made a mistake over the course of the interaction by asserting that Mahler only composed symphonies. Thus, A0 is inconsistent, whence, e.g., A0 ALC MahlerSymphony5 : ¬Symphony, despite the interlocutor’s correct classification of MahlerSymphony5. Any simple mistake that triggers a similar inconsistency in an intentional knowledge base will, therefore, entirely warp the picture of the interlocutor’s domain knowledge.
Case II: Assessing an Interlocutor’s Goals Consider a further case in which an artificial conversational agent is tasked with directing interlocutors to resources. The appropriateness of resources will undoubtedly be measured in terms of how well those resources fit the interlocutor’s goals. Such cases might see the initial interactions leveraged to populate an intentional knowledge base representing the interlocutor’s goals or requirements. Example 2 A conversational agent assists an interlocutor Self in an online technology storefront. The interlocutor’s goals are represented by the following ABox:
A1 = {Self : ∃purchases.GamingComputer ⊓ DesktopComputer} As in Example 1, there is a need for some deductions under which A1 is closed. Suppose that the artificial agent has a directive such that whenever an interlocutor counts Self : ∃purchases.DesktopComputer ⊓ GamingComputer as a goal, the interlocutor should be directed to a particular resource (e.g., a webpage). However, this trigger condition is not explicitly included in A1; it must be inferred.
However, given A1, ALC delivers additional inferences under which a collection of goals clearly should not be closed. For example, we should hesitate to license an inference to the further goal of Self : ∃purchases.(TernaryComputer ⊔ (GamingComputer ⊓ DesktopComputer)) ⊓ (GamingComputer ⊓ DesktopComputer) Despite equivalence with the member of the interlocutor’s explicit goal from A1, to count the above as a goal has several shortcomings. For one, the sentence is a bit of a red herring—one can imagine that, if read lazily, resources may be wasted on trying to connect the user with an instance of TernaryComputer.
This candidate becomes more problematic when one considers the matter
of awareness. The notion, identified in [
How can someone say that he knows or doesn’t know about p if p is a concept he is completely unaware of?[9, p. 40] This notion of awareness, in the present context, can be recast as a matter of conceptual proficiency. If a knowledge base hT , Ai is, e.g., a representation of an agent’s goals, it is implausible to say that a : C is among those goals in cases in which the agent fails to grasp the use of C, i.e., is unaware of how to distinguish cases in which a falls under C from cases in which a does not fall under C.
Given the intended interpretation, the concept TernaryComputer is a highly esoteric one. As the typical consumer of computer products—e.g. the interlocutor of Example 2—is unlikely to count the above as a goal, to assume its equivalence would be counterproductive to the aims of the conversational agent. Thus, pragmatic considerations demonstrate the problematic overgeneration following from the application of ALC to this domain.
Note that the suggestion that ALC is too strong is not to say that ALC fails as a characterization of normative dimensions of logic. Indeed, it remains plausible that e.g. α ought to accept ϕ given other beliefs. What is implausible, however, is that ALC—and a fortiori more expressive description logics like SROIQ— captures the descriptive dimension, that is, a characterization of the closure of the occurrent beliefs of an agent α.
ALCAC and ALCS⋆
We now introduce two subsystems of ALC (in the same language) that are
arguably more appropriate to the closure of intentional knowledge bases than
stock ALC. The propositional deductive system that serves as the basis for both
proposals is the logic of analytic containment AC introduced by Richard Angell
in [
The interpretation of AC offered in [
[
The present interpretation of the truth values of [
As the truth values of AC and Sf⋆de are based on weak Kleene logic wK, the model
theory for the description logics ALCAC and ALCS⋆ will reference wK as well.
The weak truth functions ∼˙ , ∧˙ , and ∨˙ are defined as follows:
Definition 1 The weak Kleene truth tables are:
∼˙
t f
e e
f t
∧˙ t e f
t t e f
e e e e
f f e f
∨˙ t e f
t t e t
e e e e
f t e f
As observed in [
We’ve noted that the presentation of AC is bilateral —one coordinate tracking
truth, the other falsity. The truth function for negation ∼¨, then, merely toggles
truth and falsity, i.e., exchanges the coordinates of a truth value. DeMorgan’s
laws suggest that extending this bilateralism to the truth functions requires that
one weak Kleene truth function operates on the arguments’ first coordinates
while its dual truth function operates on their second coordinates.
Definition 3 The AC truth functions ∼¨ , ∧¨, and ∨¨ are defined so that:
– ∼¨ (hu, vi) = hv, ui
– hu0, v0i ∧¨ hu1, v1i = hu0 ∧˙ u1, v0 ∨˙ v1i
– hu0, v0i ∨¨ hu1, v1i = hu0 ∨˙ u1, v0 ∧˙ v1i
Quantifiers will be defined over sets X of pairs of values from V32—i.e., pairs of
pairs of Kleene truth values. For convenience, let πi,j map values hhu0, v0i, hu1, v1ii
to the pair of the ith coordinate of hu0, v0i and the jth cordinate of hu1, v1i and
let πi,j[X] be the image of X under πi,j . Then:
Definition 4 The AC restricted quantifiers ∃¨ and ∀¨ are defined so that:
– ∃¨(X ) = h∃˙ (π0,0[X ]), ∀˙(π0,1[X ])i
– ∀¨(X ) = h∀˙ (π0,0[X ]), ∃˙(π0,1[X ])i
Most of the interpretative work is being done by the weak Kleene interpretation,
with the AC functions merely imposing a bilateral reading. The presentation of
the proper AC model theory is necessarily brief; for detailed discussion of the
connectives or quantifiers, see [
We now can define the model theory for ALCAC and ALCS⋆ , starting with an interpretation: Definition 5 An interpretation over V32 is a function I paired with domain ΔI , described by the following clauses: – I(a : ⊤) = he, vi and I(a : ⊥) = hv, ei for some v ∈ V3 – I(a : C) ∈ V32 and I(ha, bi : r) ∈ V 2
3 – I(a : ¬C) = ∼¨ I(a : C) – I(a : C ⊓ D) = I(a : C) ∧¨ I(a : D) – I(a : C ⊔ D) = I(a : C) ∨¨ I(a : D) – I(a : ∃r.C) = ∃¨({hI(ha, bi : r), I(b : C)i | b ∈ Δ}) – I(a : ∀r.C) = ∀¨({hI(ha, bi : r), I(b : C)i | b ∈ Δ}) – I(C ⊑ D) = ∀¨({hI(a : C), I(a : D)i | a ∈ Δ}) – I(C ≡ D) = I(C ⊑ D) ∧¨ I(D ⊑ C) We call an interpretation an AC interpretation if it ranges over V32 and an Sf⋆de interpretation if it ranges over V32⋆. In either case, we say that a sentence ϕ is true in I if the first coordinate of I(ϕ) = t; a set of sentences is true if each sentence is true.
These definitions provide very natural accounts of semantic consequence for the two systems as preservation of truth. For knowledge bases hT , Ai, we define: Definition 6 hT , Ai ALCAC ϕ if for all AC models, ϕ is true if T ∪ A is true Definition 7 hT , Ai ALCS⋆ ϕ if for all Sf⋆de models, ϕ is true if T ∪ A is true 3.2
The logics ALCAC and ALCS⋆ can be provided sound and complete tableau
calculi over a common set of rules, differing only on closure conditions for branches.
The calculi are signed, where each node is of the form [v] ϕ, for a sentence ϕ
and Kleene truth value v. For elegance, we also include two additional signs: m
(understood as not-e) and n (understood as not-t). Following the notation of [
Definition 8 The collection of rules ALC-AC is defined by the following rules: where v is any element of V3, c or c′ are new to a branch, and d is arbitrary.
Definition 9 A tableau with rules from ALC-AC fits hT , Ai ⊢ ϕ if its initial segment is some permutation of the signed sentences [t] τ for each τ ∈ T , [t] α for each α ∈ A, and [n] ϕ.
We need two notions of closure of a branch in order to define tableau calculi for the two systems.
Definition 10 A branch of a tableau with rules from ALC-AC is AC-closed if there is a sentence ϕ and distinct v, v′ ∈ V such that [v] ϕ and [v′] ϕ are on the branch.
Definition 11 A branch of a tableau with rules from ALC-AC is S-closed if it is either AC-closed or there is a sentence a : C and distinct v, v′ ∈ V such that [v] a : C and [v′] a : ¬C are on the branch where either v = e or v′ = e. If every branch of a tableau is AC -closed (respectively, S -closed), we simply say that the tableau itself is AC -closed (respectively, S -closed). Deducibility for the two systems is naturally defined as the appropriate type of closure. For a knowledge base hT , Ai, Definition 12 hT , Ai ⊢ALCAC ϕ if every fitting tableau is AC-closed Definition 13 hT , Ai ⊢ALCS⋆ ϕ if every fitting tableau is S-closed
Formal Results on ALCAC and ALCS⋆
The systems ALCAC and ALCS⋆ arise from—and are thus embeddable in—the
systems with restricted quantification introduced in [
We can recover soundness and completeness by taking advantage of this embedding with the following translation: Definition 14 The translation ·τ from LALC to the first-order language LACrQ – (a : C)τ = C(a) and (ha, bi : r)τ = r(a, b) for primitive C and r – (a : ¬C)τ = ∼(a : C)τ – (a : C ⊓ D)τ = (a : C)τ ∧ (a : D)τ and (a : C ⊔ D)τ = (a : C)τ ∨ (a : D)τ – (a : ∀r.C)τ = [∀x r(a, x)](x : C)τ and (a : ∃r.C)τ = [∃x r(a, x)](x : C)τ – (C ⊑ D)τ = [∀x (x : C)τ ](x : D)τ and (C ≡ D)τ = (C ⊑ D)τ ∧ (D ⊑ C)τ The fidelity of ·τ is witnessed by four lemmas. The first two ensure modeltheoretic agreement: Lemma 1 hT , Ai ALCAC ϕ iff T τ ∪ Aτ AC ϕτ Proof. Suppose that for ALCAC and AC valuations I and I′, I(ϕ) = I′(ϕτ ) for all atoms ϕ, i.e., whenever ϕ is of the form a : C or ha, bi : r for primitive C and r. Then a simple induction on complexity of formulae establishes that the agreement lifts to complex sentences as well. Thus, every countermodel to hT , Ai ALCAC ϕ is isomorphic to a countermodel to T τ ∪ Aτ AC ϕτ and vice versa, whence hT , Ai 2ALCAC ϕ iff T τ ∪ Aτ 2AC ϕτ .
Lemma 2 hT , Ai ALCS⋆ ϕ iff T τ ∪ Aτ Sf⋆de ϕτ Proof. As ALCS⋆ models are a fortiori ALCAC models (mutatis mutandis for ALCS⋆ ), this lemma follows immediately from Lemma 2.
Lemma 3 hT , Ai ⊢ALCAC ϕ iff T τ ∪ Aτ ⊢ACrQ ϕτ
Proof. The rules ALC-AC are selected to agree with those of the tableaux
calculus ACrQ of [
Lemmas 1–4 suffice to show the adequacy of the proof theory with respect to
the semantics. We conclude the section with the following theorems:
Theorem 1 hT , Ai ⊢ALCAC ϕ iff hT , Ai ALCAC ϕ
Proof. By Lemma 3, the left-hand side is equivalent to T τ ∪ Aτ ⊢ACrQ ϕτ .
By the results of [
As knowledge-driven, conversational artificial intelligence is introduced to more domains, the necessity of knowledge representation over intentional contexts becomes increasingly pressing. The above discussion is intended as an opening move to address this problem by proffering of two natural candidate solutions.
Much remains to be done, e.g., determination of complexity of the calculi, producing implementations of the systems, and empirical verification—or refutation—that ALCAC and ALCS⋆ are found satisfactory by users. We conclude, though, by providing some examples that bear on the issues described in Examples 1 and 2, showing that the above systems are sufficiently strong for the cases but weak enough to avoid the overgeneration of stock ALC. Example 3 Let A = {a : C, a : D}. Then A ALCAC C ⊓ D ⊑ C. We provide the following tableau demonstrating this fact: [e][a : C ⊓ D] [e][a : D] × [f][c′ : D] [e][c′ : D] [[uv00]][[aa :: DC]] · · · [ui−1][a : C]
× × × [vi−1]×[a : D] N.b. that because for each j < i, either uj = e or vj = e, each branch beneath [e][a : C ⊓ D] will close.
A similar tableau proof can be easily produced (and is thus left to the reader) demonstrating that if A = {a : C ⊓ D}, then A ALCAC a : D ⊓ C, as Example 2 required.
However, the forms of problematic inferences identified in Examples 1 and 2 can be shown to fail in ALCAC and ALCS⋆ . For example, Example 1 identified that in ALC, one inconsistent classification of a term corrupts all of an agent’s correct classifications in an ABox. Such mistakes are not catastrophic in ALCAC: Example 4 Let A = {a : C, b : ¬C, hm, bi : r, m : ∀r.C}. Then A 2ALCAC a : ¬C. A model in which I(a : C) = ht, fi, I(b : C) = ht, ti, and I(hm, bi : r) = ht, fi can be recognized as a counterexample.
Example 2 identified how the closure of an ABox under ALC may introduce subject-matter with which an agent is unaware or inproficient. The following shows how ALCAC prevents this: Example 5 Let A = {a : C}. Then A 2ALCAC a : C ⊓ (C ⊔ D). A model in which I(a : C) = ht, fi and I(a : D) = he, ei can be confirmed to be a counterexample. Of course, the adequacy of the systems introduced here will be determined by user’s experiences with implementations. Prior to such surveys, however, they at least can be seen to enjoy a superior fit to the use-cases than ALC and can therefore be recognized as a step in the right direction.
A reviewer has remarked that Example 3 reflects an inability to reason from an empty ABox. In the systems described in this paper, one is not prevented from reasoning from an empty TBox and ABox. But an empty TBox and ABox pair is agnostic about an agent’s awareness, constituting insufficient grounds to infer anything about the concepts with which an agent is familiar or proficient.