The Felony Score Sheet used in the US State of Florida, describes various features of a crime and their assigned points. Features may include `possession of cocaine', or `number of caused injuries'. A threshold must be reached to decide compulsory imprisonment. In previous research, we have introduced a perceptron operator for knowledge representation languages. With it, concepts can be de ned by listing a concept's features with associated weights, and a threshold. An individual belongs to such a concept if the weighted sum of the listed features it belongs to reaches the threshold. It can capture the concept of compulsory imprisonment de ned by the Felony Score Sheet. However, it su ers some limitations in that one must arti cially use concepts like `caused one injury', `caused two injuries', etc, to be able to count. This paper proposes an extension of the perceptron operator to de ne concepts like the compulsory imprisonment from the Felony Score Sheet faithfully and easily, relying on role-successors counting. We show that when the weights are non-negative, reasoning in ALC augmented with the perceptron operator can be reduced to reasoning in ALCQ. Capitalizing on the recent ALCSCC, we also show that adding the operator to ALC does not a ect the complexity of reasoning in general.
The Felony Score Sheet used in the State of Florida1, describes various features of a crime and their assigned points. A threshold must be reached to decide compulsory imprisonment. For example, if the primary o ence is possession of cocaine, then it corresponds to 16 points, one victim injury describable as \moderate" corresponds to 18 points, and a failure to appear for a criminal proceeding results in 4 points. Imprisonment is compulsory if the total is greater than 44 points and not compulsory otherwise.
In [
rrt(C1 : w1 : : : Cn : wn)
Xfwi j d 2 (Ci)I g
t :
We call it the threshold or perceptron operator, or \tooth". Adding the
perceptron operator to ALC does not increase the expressivity, since every instance
of the operator can be replaced with an equivalent boolean expression. In [
A knowledge base describing the laws of Florida would need to represent this score sheet as part of its de nition of its CompulsoryImprisonment concept, for instance as
rr44(CocainePrimary : 16; ModerateInjuries : 18; : : :) : The Felony Score Sheet is slightly more complicated, though. For instance, 18 points are added for every instance (every count) of a `moderate injury victim'.
Of course we can use one concept 1MI, 2MI, 3MI, ... for each number of moderate injury. With all of them pairwise disjoint and with weights 18, 36, 54, ... we can use
rr44(CocainePrimary : 16; 1MI : 18; 2MI : 36; 3MI : 54; : : :) :
rr44(CocainePrimary : 16; 1MI : 18; 2MI : 18; 3MI : 18; : : :) : No matter what, one must decide what will be the maximum number of moderate injuries that are taken into account, introduce new concepts (and possibly axioms in the TBox), multiply weights, and write them all into a perceptron operator.
Isn't there some more exible way to specify this kind of concepts? The problem at hand is to investigate how to extend the rr operator to accommodate the Florida example faithfully and with simplicity. In this paper, we extend the regular tooth with role-successor counting abilities.
Related work. [
[
Outline. We present ALCSCC1 in Section 2, and de ne ALC and ALCQ as fragments. In Section 3 we introduce our extension of the tooth with counting capabilities. In Section 4, we show how to embed into ALCQ the logic ALC equipped with the new perceptron operator where the weights are positive. The embedding su ces to show that reasoning can be done in 2ExpTime when the threshold is expressed in binary, and that it is ExpTime-complete when the threshold is expressed in unary. Section 5 provides an embedding into ALCSCC1, showing that ALC equipped with the new perceptron operator is ExpTimecomplete in general. In Section 6, we brie y suggest a further way to extend the perceptron operator. Section 7 concludes. 2
ALC and its extensions with cardinality restrictions
We present ALCSCC1 and its well-known fragments ALC and ALCQ. See [
QFBAPA1. The Description Logic ALCSCC1 uses formulas of the quanti erfree Boolean algebra with Pressburger arithmetic (QFBAPA) to express constraints on role successors.
QFBAPA over nite integers is presented in [
A QFBAPA1 formula F is a Boolean combination of set and numerical constraints like AT .
AB ::= B = B j B
F ::= AT j AB j :F j F ^ F j F _ F
B AT ::= T = T j T < T
T ::= k j K j jBj j T + T j K B ::= x j ; j U j B [ B j B \ B j B
T
K ::= 0 j 1 j 2 j : : : Set terms like B are obtained by applying intersection, union, and complement to set variables and constants ; and U . Set constraints like AB are of the form B1 = B2 and B1 B2, where B1; B2 are set terms like B.
Presburger Arithmetic (PA) expressions T are built from variables, nonnegative integer constants from K, and set cardinalities jBj, and then closed under addition as well as multiplication with non-negative integer constants from K. They can be used to form the numerical constraints AT , namely of the form T1 = T2 and T1 < T2, where T1; T2 are PA expressions of type T .
The semantics of set terms B is de ned using substitutions that assign a set (U ) to the constant U and subsets of (U ) to set variables. The evaluation of all set terms under is done using the rules of set theory.
Set constraints of the form AB are evaluated to true or false under , also by using the rules of set theory.
Then the domain of is extended to PA expressions T by assigning to them an element of N [ f1g. The cardinality expression jBj is evaluated as the cardinality of (B) if B is nite, and as 1 if it is not. The evaluation of all PA expressions under is done using the rules of addition and multiplication (extended with in nity as above).
Numerical constraints AT are evaluated to true or false under , under the rules of basic arithmetic.
Finally, a solution of a QFBAPA1 formula F is a substitution that evaluates F to true, using the rules of Boolean logic.
Syntax of ALCSCC1. Let NC and NR be two disjoint sets of concept names, and role names, respectively.
The set of ALCSCC concept expressions over NC and NR is de ned as follows:
C ::= A j :C j C u C j C t C j succ(F ) ; where A 2 NC , F is a QFBAPA1 formula using role names and ALCSCC concept expressions over NC and NR as set variables.
An ALCSCC1 TBox over NC and NR is a nite set of concept inclusions of the form C v D, where C and D are ALCSCC1 concept expressions over NC and NR. We write C D to signify that C v D and D v C. Semantics of ALCSCC1. Given nite, disjoint sets NC and NR of concept and role names, respectively, an interpretation I consists of a non-empty set I and a mapping I that maps every concept name C to a subset CI I and every role name R 2 NR to a binary relation RI I I . Given an individual d 2 I and a role name R 2 NR, we de ne RI (d) as the set of R-successors. We de ne ARSI (d) as the set of all successors of d. The mapping I is extended to Boolean combinations of concept expressions in the obvious way.
Successor constraints are evaluated according to the semantics of QFBAPA1. To determine whether d 2 (succ(F ))I , U is evaluated as ARSI (d), the roles occurring in F are substituted with RI (d), and the concept expressions C occurring in F are substituted with CI \ ARSI (d).
Then, d 2 (succ(F ))I is true i this substitution is a solution of the QFBAPA1 formula F .
The interpretation I is a model of the TBox T if for every concept inclusion C v D in T , it is the case that CI DI .
A concept expression C is satis able wrt. the TBox T if there exists a model of the TBox such that CI 6= ;.
Example 1. In the ALCSCC1 formula succ(jcausesj < 2), 2 is an integer constant (also a PA expression), causes is a role, but also a set term, jcausesj is a set cardinality (also a PA expression), and jcausesj < 2 is a numerical constraint.
When deciding whether d 2 (succ(jcausesj < 2))I , we build the substitution , such that (2) = 2, and (causes) = causesI (d).
Let I be an interpretation, and suppose that d has 2 causes-successors, namely d1 and d2 (and nothing else). We then have (causes) = fd1; d2g, (jcausesj) = 2, and (jcausesj < 2) = f alse. There are no other possible substitutions to consider. So d 62 (succ(jcausesj < 2))I .
Suppose that we also have InjuryI = fd2; d3; d4g, and (d; d3) 2 hasI (but nothing else).
When deciding whether d 2 (succ(jcauses \ Injuryj = 1))I , Injury is a concept description but also a set term, and we build the substitution 0 such that 0(1) = 1, 0(causes) = causesI (d) = fd1; d2g, 0(Injury) = InjuryI \ ARSI (d) = fd2; d3g, 0(causes \ Injury) = 0(causes) \ 0(Injury) = fd2g, 0(jcauses \ Injuryj) = 1, and 0(jcauses \ Injuryj = 1) = true. Hence 0 is a solution of the QFBAPA1 formula jcauses \ Injuryj = 1. So d 2 (succ(jcauses \ Injuryj = 1))I .
ALC and ALCQ. ALCQ is the fragment of ALCSCC1 such that succ(F ) is of the form succ(jR\Cj n) or succ(jR\Cj n), where C is a concept expression and R 2 NR, and n 2 N. ALC is the fragment of ALCSCC1 such that succ(F ) is of the form succ(jR \ Cj 1).
Hence, we can de ne 9R:C = succ(jR \ Cj 1), ( n R:C) = succ(jR \ Cj n), and ( n R:C) = succ(jR \ Cj n). Quali ed cardinality restrictions of ALCQ are equivalently de ned as: ( n R:C)I = d 2 and ( n R:C)I = d 2 I jfc 2 We de ne (= n R:C) = ( n R:C) u ( n R:C). We de ne a new collection of perceptron operators, that we call simply counting teeth:
C = rrt C1 : w1; : : : ; Cp : wp j (R1; D1) : m1; : : : ; (Rq; Dq) : mq ; where w~ = (w1; : : : ; wp) 2 Zp, m~ = (m1; : : : ; mq) 2 Zq, t 2 Z, Ci and Di are concepts expressions and Ri are roles. (The tooth from our previous work, without role-successor counting will be called regular tooth.)
With caused a role, we can now faithfully de ne the concept CompulsoryImprisonment of the Felony Score Sheet: rr44 CocainePrimary : 16;
j (caused; ModerateInjury) : 18; : : : : Semantics. When an individual d has only a nite number of Di-successors in I, or when the weights are all non-negative, then the value of a d 2 I under the counting tooth C is:
When the individual d can have an in nite number of Di-successors and some weights are positive and others are negative, then vCI (d) can be ill-de ned. (I.e. what should be the value of 1 1?) So instead of the single value vCI (d), we introduce two values, vCI 0(d) and vCI<0(d), that represent the sum of the non-negative summands and the sum of the negative summands, respectively. fwi j d 2 CiI g+ (mi jfc 2
I j (d; c) 2 RiI ^c 2 DiI gj) : vCI 0(d) = vCI<0(d) =
X
X i2f1;:::;pg
wi 0 i2f1;:::;pg wi<0
X
X i2f1;:::;qg
mi 0 i2f1;:::;qg
mi<0 fwi j d 2 CiI g+ (mi jfc 2
I j (d; c) 2 RiI ^c 2 DiI gj) : Clearly vCI 0(d) 0 and vCI<0(d) 0.
Finally, the semantics of C in a possibly in nite-branching interpretation I is given as follows:
CI = fd 2
I j vCI 0(d)
t vCI<0(d)g : Example 2. For purposes of illustration we de ne a `Modi ed Compulsory Imprisonment' as
MCI = rr44 CocainePrimary : 16 j (caused; ModerateInjury) : 18); (preventiveDetention; Month) : 1 ; where only cocaine possession as primary o ence and the number of moderate injuries are kept from the original score sheet, and where in addition every month of preventive detention lowers the score by one.
We want to decide whether the felony d 2 I falls within the de nition of this modi ed compulsory imprisonment, under the assumptions that d is not in CocainePrimaryI , that jpreventiveDetentionI (d) \ MonthI j = 12, and jcausedI (d) \ ModerateInjuryI j = 3.
So, we have: vMICI 0(d) = 0 + 3 18 = 54 and vMICI<0(d) = 12 ( 1) = 12. We must evaluate vMICI 0(d) t vMICI<0(d), which is 54 44 + 12, or 54 56, which is false. So d does not fall within the modi ed compulsory imprisonment. 4
Particular case: Embedding ALC with counting teeth with non-negative weights into ALCQ, and preliminary complexity results In practice, negative weights are not always necessary. As evidence, one can observe that the Felony Score Sheet does not contain negative points for computing the total number of points.
Let us then rst restrict our attention to counting teeth rrt C1 : w1; : : : ; Cp : wp j (R1; D1) : m1; : : : ; (Rq; Dq) : mq such that m~ 2 Nq. In this section we will still allow the weights on the concepts to be negative: w~ 2 Zp. For regular teeth, we stipulate that the weights are non-negative simply for brevity, and because it does not really matter. Indeed, a regular tooth with negative weights on concepts can be transformed e ciently into a regular tooth with only non-negative weights on concepts, as shown in [14, Prop. 3].
We show that the language ALC equipped with counting teeth rr is no more expressive than ALCQ (Prop. 1) when the weights are non-negative. We show that reasoning can be done in 2ExpTime when the threshold is expressed in binary and in ExpTime when it is expressed in unary (Prop. 2). We will improve upon the 2ExpTime upper-bound in Section 5. However, this section has the merit to show how one can transform the problem of reasoning with ALC equipped with the counting tooth with non-negative weights into a problem of reasoning with ALCQ (although ine ciently when the threshold is encoded in binary), for which e cient reasoning tools exist. We leave for future work whether an e cient embedding into ALCQ is possible even when the threshold is encoded in binary.
Let us observe that ALC equipped with counting teeth restricted to nonnegative weights is strictly less expressive than when negative weights are allowed. Indeed, one can express \has as many sons as daughters": AsMany =rr0 rr 0 j (isParentOf; Boy) : 1; (isParentOf; Girl) : 1 u j (isParentOf; Girl) : 1; (isParentOf; Boy) : 1 :
This cannot be expressed in ALCQ [6, Lemma 2], but ALC equipped with counting teeth with non-negative weights has the same expressivity as ALCQ (Prop. 1).
We recall that, in contrast, adding the regular tooth of [
Now de ne the counting tooth
C0 = rrt C1 : w10; : : : ; Cp : wp0; E1 : wp0+1; : : : ; Er : wp0+r j
(R2; D2) : m2; : : : ; (Rq; Dq) : mq where: Lemma 1.
{ wi0 = wi, for 1 i p { wp0+i = i m1, for 1
i r { r = l t+P1mi1 p jwi0j m (in fact it's enough to sum only jwi0j when wi0 < 0) { Ei = (= i R1:D1), for 0 i r 1 { Er = ( r R1:D1)
(C)I = (C0)I : Proof. We must show that for d 2 I , we have vCI 0(d) t vCI<0(d) i vCI0 0(d) t vCI0<0(d).
To make the proof smoother, we can start with a simple observation. When C = rrt C1 : w1; : : : ; Cp : wp j (R1; D1) : m1; : : : ; (Rq; Dq) : mq and m~ 2 Nq, then for every d 2 I we have vCI (d) t i vCI 0(d) t vCI<0(d). Indeed, when m~ 2 Nq, then vCI<0(d) is nite. So vCI 0(d) + vCI<0(d) is well de ned and equal to vCI (d).
To prove the lemma, we can then verify that for d 2 I , we have vCI0 (d) t i vCI (d) t. We can see that vCI (d) vCI0 (d). So if vCI0 (d) t, then vCI (d) t. Hence it su ces to verify that if vCI (d) t then vCI0 (d) t.
Let k be the number of R1-successors of d that are in D1I .
If k r, we can focus speci cally on the contributions of (R1; D1) : m1 in vCI (d) and of all Ei : wp0+i in vCI0 (d). The contribution of (R1; D1) : m1 in vCI (d) is k m1, and (when k r), so is the contribution of all Ei : wp0+i in vCI0 (d). Then clearly, vCI0 (d) = vCI (d), so vCI0 (d) t i vCI (d) t.
It remains to verify the case of k > r. We must show that if vCI (d) t then vCI0 (d) t. When k > r, the contribution of all Ei : wp0+i in vCI0 (d) is r m1; so vCI0 0(d) is bounded below by r m1. Since we only consider teeth with m~ 2 Nq in this section, vCI0<0(d) is bounded below by P1 i p jwi0j. So vCI0 (d) = vCI0 0(d) + vCI0<0(d) l t+P1mi1 p jwi0j m m1 P1 i p jwi0j. So vCI0 (d) t. Example 3. With C = rr3 C1 : 2 j (R; D) : 1 , we have r = d(3 + 2)=1e = 5. The rationale is that if an individual is a C1 it is still su cient for it to have 5 R-successors that are D for this individual to be a C. If it is not a C1, then 3, 4, 5 or more R-successors that are D are su cient.
We get C0 = rr3 C1 : 2; (= 1 R:D) : 1; (= 2 R:D) : 2; (= 3 R:D) : 3; (= 4 R:D) : 4; ( 5 R:D) : 5 j . Of course, it is equivalent to the regular tooth C00 = rr3 C1 : 2; (= 1 R:D) : 1; (= 2 R:D) : 2; (= 3 R:D) : 3; (= 4 R:D) : 4; ( 5 R:D) : 5 .
So a counting tooth with ALC concepts can be transformed into a regular
tooth with ALCQ concepts when only non-negative weights are allowed. In turn,
we know how to (e ciently) transform it into an ALCQ concept [
Proposition 1. ALC with counting teeth with non-negative weights has the same expressivity as ALCQ.
Preliminary complexity results. In the rewriting above, the size of the tooth strictly grows, as one pair (R1; D1) is removed, but r new concepts are added, each of size larger than the combined sizes of R1 plus D1. Yet, r is bounded by the threshold t. So, when the threshold is expressed in unary, the rewriting only causes a linear expansion. But if the weights are encoded in binary, this is not an e cient rewriting! It only yields this partial result.
Proposition 2. Reasoning with ALC with counting teeth, disallowing non-negative weights, wrt. to a TBox, is in 2ExpTime. When the threshold is represented in unary, then it is ExpTime-complete.
Proof. When deciding whether the concept C is satis able wrt. T , (1) if there are nested counting teeth (in T or C), pick the inner-most (breaking ties at random) tooth concept (T ), (2) introduce a fresh concept name F reshT , (3) repeat 1{2, with C := C[T =F reshT ] is satis able wrt. T := T [T =F reshT ] [ fF reshT T g, (where X[A=B] stands for the uniform substitution with B of every occurrence of A in X).
The number of teeth in T and C is linear in the size of T and C, so the procedure above terminates in polynomial time, and results in a combined size of the T and C that are linear in the combined size of T and C at the start of the procedure.
Now, observe that: { C is satis able wrt. T i
fF reshT T g. { when the procedure halts, there are no more nested teeth in T and C.
C[T =F reshT ] is satis able wrt. T [T =F reshT ] [
It now su ces to transform all the counting teeth in the resulting T and C into regular teeth applying iteratively the rewriting proposed above. We obtain T and C which are now written in ALCQ equipped with regular teeth. It causes a blow-up in size exponential in the larger threshold of an occurring counting tooth, when represented in binary, and only a polynomial increase when the thresholds are represented in unary.
Finally, using the transformations of [
General case: Embedding ALC with counting teeth into ALCSCC1 In Section 4, we failed to establish a precise complexity of ALC with counting teeth, even restricting our attention to only non-negative weights for roles. Here we embed it into ALCSCC1, showing that the complexity is in ExpTime.
This approach has a practical drawback: ALCSCC1 is not a logic supported by the existing reasoning services, and algorithms t for implementation do not exist. But it will allow us to pin down the complexity of reasoning in ALC augmented with counting tooth operators.
Let C = rrt C1 : w1; : : : ; Cp : wp j (R1; D1) : wp+1; : : : ; (Rq; Dq) : wq . Let us assume for now that C does not have nested teeth. Let T be a TBox. Let us assume for now that T is an ALC TBox (without teeth).
We want to decide whether the concept description C is satis able wrt. the TBox T .
We add a fresh role name zooCi (`zero-or-one') adding the axioms (= 1 zooCi :>) Ci and (= 0 zooCi :>) :Ci for every 1 i p to T . We obtain the TBox T 0.
Now, we de ne summands = w1 jzooC1 \ >j; : : : ; wp jzooCp \ >j; wp+1 jR1 \ D1j; : : : ; wq jRq \ Dqj : Roughly speaking, C is the set of individuals such that the sum of the elements of summands is greater or equal to t. The quantity jzooCi \ >j will be 1 if the individual is a Ci and 0 if it is not.
But some of these summands could be negative, exactly those where wi < 0,
and QFBAPA1 does not allow using negative constants. In [
When n 2 N, we syntactically identify n with n. If t 0, then tl = t and tr = 0, else tl = 0 and tr = t. Now consider the ALCSCC concept 0
X wi xi2summands wi<0 wi xi tr +
X wi xi2summands wi 0
1 wi xiCC :
A (In order to be totally rigorous, T1 (T1 < T2) _ (T2 = T1).) Lemma 2. C is satis able in T i C0 is satis able in T 0.
We can now do better than Proposition 2.
Proposition 3. Reasoning in ALC with counting teeth, wrt. a TBox is ExpTime-complete, even when the threshold is expressed in binary, and even when the weights on roles are allowed to be negative.
Proof. Starting from the deepest teeth (in the concept and the TBox), we rewrite
them into an ALCSCC concept as above, adding zoo role axioms into the TBox
as we go. Those are a series of polynomial transformations, all equi-satis able.
The result follows because reasoning in ALCSCC can be done in ExpTime [
In the previous extended family of teeth, the additional weights are used as multiplying factor to the number of features reached by a role.
We could envisage to replace these weights with arbitrary functions f , from N (or N [ f1g) to R. A feature with weight w could be represented by a feature with function f (n) = w n.
Now, although irremediably leaving the cosy realm of linearity, f could be anything, e.g., a polynomial, a sigmoid, a binomial distribution, etc.
We de ne a new collection of perceptron operators
C = rrt C1 : w1; : : : ; Cp : wp j (R1; D1) : f1; : : : ; (Rq; Dq) : fq ; where w~ = (w1; : : : ; wp) 2 Rp, f~ = (f1; : : : ; fq) is a q-vector of functions from N to R, Ri and Di are roles and concepts respectively.
When role-branching is nite (for simplicity of exposition), the value of a d 2 I under a C is:
X X fq(jfc 2
I j (d; c) 2 RiI ^ c 2 DI gj) :
As illustrated in [
When we do not allow negative weights, the extended perceptron operator can faithfully and easily express concepts like `compulsory imprisonment' from the Florida Score Sheet. When added to ALC, the resulting logic has exactly the same expressivity as ALCQ. We showed how reasoning can be transformed into reasoning in ALCQ, allowing one to straightforwardly use state-of-the-art reasoning services for ALCQ. When the threshold is expressed in unary, it is no more succinct. Whether it is more succinct than ALCQ when the threshold is expressed in binary remains an open question.
When we allow negative weights, the extended perceptron operator can express concepts like \has more sons than daughters", \has as many arms than legs", ... When added to ALC it yields a DL that is strictly more expressive than ALCQ, and is not anymore a fragment of FOL.
The complexity of the DL that is obtained by adding the extended perceptron operator to ALC is ExpTime-complete, no matter whether we allow negative weights or not, or whether the threshold is represented in unary or binary.