Numerical Quantifiers and Their Use in Reasoning with Negative Information

1. INTRODUCTION

Logic based reasoning programs, that is reason­ ing programs based on operators (connectives, quantifiers, modals) which have been studied as part of formal logical systems benefit from the fact that the inferential properties of their operators are clear and well known. They need not be restricted, however, to a minimal set of operators. Minimal sets of operators are useful for proving properties of logical systems such as consistency and completeness, but using a logical system for carrying out inferences is simplified (for people) by enlarging the set of basic operators. This is one reason that natu­ ral deduction systems like those of [1] , [4J and [111, with reasonable sets of connectives and two rules of inference for each one, are easier to use than axiomatic systems with

minimal sets of connectives, rules and axioms.

This paper is motivated by an interest in pra­ grams that represent knowledge, including the knowledge of rules of reasoning, and that use those rules to perform reasoning. I believe that such programs are enhanced by the availa­ bility of a large set of operators that typify and formally model as many of the modes of human reasoning as possible. This paper dis­ cusses a set of operators, the numerical quan­ tifiers, which can be implemented in reasoning

*This material is based on work supported in part by a Faculty Research Fellowship from the Research Foundation of State University of New York, and in part by the National Science

Foundation under Grant No. MCS78-02274.

programs as a single parameterized operator, and which model an important mode of human reasoning.

Numerical quantifiers, discussed briefly in ~0, pp. 63-64], are generalizations of the existen­ tial quantifier. They can be used to formalize

such statements as:

There are at least two numbers z, such that z+2<6.

T2ere are exactly two numbers x, such that

x +4=4x.

There are at most two numbers y, such that y+S<ll-2y.

(all from [10, pp. 64, 67].)

One numerical quantifier is the more commonly encountered unique existential, expressed as 3!xA(x) in the not,tion of ~. p. 199]. We will use the notation 3ixA(x) for "there exists at least i and at most j x such that A(x)". The usual existential quantifier, 3xA(x), can then be considered an abbreviation of iixA(x) (al­ though later we will make a distinction), and the unique existential becomes 3lxA(x). In general, ~xA(x) are the "numerically definite quantifiers" mentioned in ~, pp. 165, 6].

We have found the numerical quantifiers particu­ larly useful for the mode of reasoning by the process of elimination: if the maximal number of positive cases are found, the rest must be negative; if the maximal number of negative cases are found, the rest must be positive. Numerical quantifiers thus can introduce ex­ plicit negative information into a data base,

~nd can make use of negative information to derive positive information. To set the stage for this discussion, we will first discuss the role of the simple existential quantifier in deductive question-answering.

2. THE EXISTENTIAL QUANTIFIER

Let us consider statements which:

1. include an existential quantifier;
2. 2} are to be stored in the data base of a de­ ductive question-answering system (QAS};
3. 3} are to be used by the system to answer questions.

We will consider wh~t contribution such state­ ments (we call these, as well as other general statements, deduction rules) can make to the question-answering process.

Existential quantifiers can either be outside or inside the scope of universal quantifiers. If outside the scope of any universal quanti­ fier, for example "There is a man who owns a dog" or 3X(Man(x}&ay(Dog(y}6Dwns(x,y))), there is no need to retain the quantifier in the data base, one can simply create new individual con­ stants (Skolem constants) and substitute them for the quantified variables, storing, in this example, the three facts Man(ml}, Dog(dl}, and Owns(ml,dl}.

Existential quantifiers within the scope of universal quantifiers can be eliminated by re­ placing them with Skolem functions. So, (1) Every person has a mother

can be represented by yx(Person(x)~3Y(Person(y) &Mother(y,x))) or by yx(Person(x)~(Person(f(x)) &Mother(f(x),x))), where f is a new function. This rule could be used to answer the question, "Does John have a mother?", but the point of the Skolem function is that for each person a new person must be postulated to be his or her mother. So, knowing just (1), and that John is a person, if we asked "Who is John's mother?", the answer would be some individual about whom we know nothing except that she is a person and is John's mother.

It may seem strange that asking a question can cause the creation of a new individual, but consider definite descriptions that refer to individuals which have not been explicitly intJ:"oduced, as in the statement "John's mother owns a dog". Normally, we would look in the data base for John's mother and assert that she owns a dog, but in this case there is no record of John's mother in the data base. However, rule (1) justifies creating a new individual to be John's mother. "John's mother owns a dog" presupposes that John has a mother. With neither an explicit mother, nor the rule, the sentence has a failed presupposition and should not be accepted.

If the data base contained both rule (1) and "Jane is John's mother", and we input, "John's mother owns a dog," rule (1) is at best useless, and at worst, harmful. If the rule were acti­ vated, it would have to produce a new mother, and the phrase "John's mother" would be ambigu­ ous. If rule (1} were not activated, "Jane owns a dog" would be stored. This is technically wrong (consider replacing ''mother" with "parent'), but probably what the speaker intended.

In summary, existential quantifiers need be stored in the data base of a QAS only when with­ in the scope of a universal quantifier, and they are most useful for supplying referents for designating phrases with no previously explicit­ ly mentioned referent.

3. MAXIMAL NUMERICAL QUANTIFIERS

Consider the data base containing "Jane is John's mother" and the question, "Is Mary John's mother?" In order to get the correct answer, ''No", we need the rule

1. Every person has at most one mother. (We will ignore, in this paper, the problem of identity or extensional equivalence. That is, the even more correct answer, "Only if Mary is the same person as Jane". See [7] for a solu­ tion to this problem using a combination of path tracing and deductioQ rules.) Let us call quantifiers of the form :a:JxA(x), read "there exists at most j x such that A of x", maxiinal numerical quantifiers. In this notation, (2) becomes

1 (2') VX(Person(x)~ y(Person(y)&Mother(y,x)))

Unlike the simple existential quantifier, the maximal numerical quantifiers do not justify the introduction of new individuals. However, we can derive negative statements from them once the maximal number of individuals satisfy­ ing the quantified statement are known. In our example, rule (2) justifies the answer, ''No, Mary is not John's mother".

If a data base consisted of rules (1} and (2) only, and we asked, "Is Jane John's mother?", it might seem that rule (1) would create a new Skolem constant to be John's mother, and then by rule (2) the answer would be ''No". However, rule (1) must not be invoked in th~s case, be­ cause it is illegal to instantiate an existen­ tially quantified variable to a constant we already know something about. Since John's mother is not known explicitly, Jane is not ruled out and the correct answer in this case is "I don't know".

The formula aJxA(x) is therefore useful when we already know j different individuals satisfying A and are asked if a (j+l)st individual, t, also satisfies A. The formula -A(t) is then deriv­ able.

4. MINIMAL NUMERICAL QUANTIFIERS

Now consider formulas of the form, 3ixA(x), read "There exists at least i x such that A of of x". We will call quantifiers of this form, minimal numerical quantifiers. What useful in­ formation does this provide that is not provided by 3xA(x)? If the universe under discussion contains n individuals, and we already know of n-i individuals y such that ""A(y), we can de­ duce about any (n-i+l)st individual, t, that A(t). Consider five professors, three of whom are in a meeting. If I know who the five people are, and I've seen two in the hall, I can de­ duce who is in the meeting.

Since the usefulness of minimal numerical quantifiers depends on some universe of objects, it is convenient to introduce domain restricted minimal numerical quantifiers. We will use the notation 3tx(P(x):Q(x)), where P(x) and Q(x) are arbitrary formulas with x free, to mean, "of all objects x such that P(x), at least i of them satisfy Q". In a data base without the closed world assumption [5], we can seldom be sure that the objects known to satisfy P are the only ones that actually do. For example, the following corpus, representing the example above, is insufficient for deducing who is in the meeting.

1. 33x(Professor(x):In(x,meeting))
2. VX(In(x,~all)~~n(x,meeting))
3. Professor(Pat)
4. Professor(Gabor)
5. Professor(Nick)
6. Professor(John)
7. Professor(Stu)
8. In(Pat,hall)
9. In(Nick,hall)
10. However, it may be that whoever provided rule (3) knows that there are only five professors. To record such information, we will add another parameter to the minimal numerical quantifiers giving the schema, n3ix(P(x):Q(x)), where n is the number of objects which satisfy P. Notice that this amounts to a closed sub-world assump­ tion. If we replace (3) in the above corpus by

(3') 5a3x(Professor(x):In(x,meeting)) stating that '~f the five professors, at least three are in the meeting", then we can derive In(Gabor,meeting),In(John,meeting) and In(Stu, meeting).

With minimal numerical quantifiers, negative information can be used to deduce positive in­ formation. Given the rule n3ix(P(x):Q(x)), and n-i individuals y such that P(y)&~(y), we can deduce for any other individual t such that P(t) holds that Q(t) also holds.

5. NUMERICAL QUANTIFIERS

The minimal and maximal numerical quantifiers can be combined into what we ~hall simply call the numerical quantifiers, n3ix(P(x):Q(x)), which are read, "Of the n individuals x such that P(x), at least i and at most j are such that Q(x)", or simply, "Between i and j of the n Ps are Qs". The other quantifiers we have discussed may be obtained by leaving out appropriate parts of this schema.

If.a data base contains a rule of the form nafx(P(x):Q(x)) and j individuals are found satisfying P(x)&Q(x), it may be deduced that the remaining n-j individuals satisfying P(x) satisfy-Q(x). However, ifn-i individuals are found to satisfy P(x)&-Q(x), it may be de­ duced that the remaining i individuals satisfy­ ing P(x) also satisfy Q(x).

The regular existential quantifier, 3xA(x), is the same as the numerical quantifier aixA(x). It is now clear why it seldom helps us deter­ mine whether A(t) holds for a fixed individual, t. aixA(x) cannot derive ~(t), since there is no maximum -- all individuals might satisfy A. It can seldom produce A(t), since that would require knowing that all other individuals satisfy ~A, and we rarely have a finite list of all the individuals in the domain. Because of this, the implementor of a deductive QAS may wish to distinguish the existential quantifier from the numerical quantifiers, and continue to prohibit invocation of a rule that would bind an existentially quantified variable to a con­ stant.

6. NUMERICAL QUANTIFIERS IN SNePS

Numerical quantifiers have recently been added to SNePS, the Semantic Network Processing System @; 8], which already included universal and existential quantifiers as well as a set of non-standard connectives. SNePS accepts numeri­ cally q~antified formulas of the form (12) natR"(Pl(X), ... ,fk(x):Q(x)) (13) n~'X(Pl(X), ... ,Pk(X):Q(x)) ( 14) alx(P 1 ('x), .. . , Pk (x): Q(X)) where k~O and x represents a sequence of variables <x1, ... ,~ each of which is free in at least one of P1(x), ... ,Pk(x),Q(x). The meaning of (12) is that there are n sequences of individuals, <t1·· . . ,tm> such that (Pl(XJ& ... &Pk("X)) [t1/x1, ... ,tmiXm] is true and that at least i and at most j of these n sequences also satisfy Q(x). The meanings of (13) and (14) are the appropriate simplifications of this.

As an example of (12), consider the many-many relationship of dog ownership. Several people may jointly own one dog, and several dogs may be ~ed by the same person. The formula s32x,y(Person(x),Dog(y),Owns(x,y):Spoils(x,y)) says that of the five dog ownership relations (e.g. <John, Rover>, <John,Spot> ,Qane ,Spot>, <Mary, Lassie>, and <Jim,Lassie>), between two and four involve spoiling the dog.

Rules of the form of (12) are represented in the SNePS network by a node with: an auxiliary arc labeled EMIN to i; an auxiliary arc labeled EMAX to j; an auxiliary arc labeled ETOT to n; descending arcs labeled PEVB to the nodes representing the variables in x; descending arcs labeled ~NT to the nodes representing the formulas P1(x), ... ,Pk(x); a descending arc labeled CQ to the node representing Q(x).In SNePS, auxiliary arcs may connect semantic net­ work nodes to arbitrary data structures, in­ cluding numbers. A descending arc goes from a network node to another network node and has a paired ascending arc in the reverse direction.

7. EXAMPLES

In this section, we will show SNePS runs of the three major numerical quantifier examples from above. Lines beginning with "**" or "*" were typed by the user. The character";" indicates that the rest of the line is a comment. Input is in SNePSUL, the SNePS User Language, [8). Each input and each deduced fact is commented by its English translation. Each rule is also c~ented by its translation into the logical syntax used previously in this paper. The runs were transcribed to make them easier to read, and edited only to add the comments and to re­ move some trace printing. SNePS is written in Lisp and runs interactively on a CYBER 173. A compiled version was used for these examples.

7.1 Example.!

We assert that Jane is John's mother and that everyone has at most one mother. Then we ask if Mary is John's mother, and SNePS responds that she is not.

**;Jane is a person. *(BUILD MEM JANE CLASS PERSON) (Ml3) ;The SNePS node representing the assertion. 8 MSECS **;John is a person. *(BUILD MEM JOHN CLASS PERSON) (M14) 8 MSECS **;Jane is John's mother. *(BUILD A JANE R MOTHER 0 JOHN) (Ml5) 12 MSECS

**;Every person has at most one mother.

*;Vx[Person(x)~3ly(Person(y) : Mother(y,x))]

*(BUILD AVB $X * ANT (BUILD HEM *X CLASS PERSON) * CQ (BUILD EMAX 1 PEVB $Y * ~NT (BUILD MEM *Y CLASS PERSON) * CQ (BUILD A *Y R MOTHER 0 *X))) (M21) 65 MSECS **;Mary is a person. *(BUILD MEM MARY CLASS PERSON) (M22) 7 MSECS **;Is Mary John's mother? * (DESCRIBE (DEDUCE A MARY R MOTHER 0 JOHN)) (M24 (MIN(O)) (MAX(O)) (ARG(M23))) ; It is not the case that (M23 (A(MARY)) (R(MOTHER)) (O(JOHN))) ; Mary is the mother of John. (DUMPED) 1120 MSECS

7.2 Example 2

At least three of the five professors are in the meeting. We see Pat and Nick in the hall. When we ask who is in the meeting, SNePS deduces that Pat and Nick are not, but Gabor, John, and Stu are.

**;At least 3 of 5 professors are in a meeting. *; 5:il3x (Professor(x)-:;>In(x,meeting~ *(BUILD ETOT 5 EMIN 3 PEVB $X * ~NT (BUILD MEM *X CLASS PROFESSOR) * CQ (BUILD A *X R IN 0 MEETING))

(M4) 44 MSECS **;Whoever is in the hall is not in the meeting. *; VX[In(x,hall)~ -In(x,meeting)] *(BUILD AVB $X * ANT (BUILD A *X R IN 0 HALL) * CQ (BUILD MIN 0 MAX 0 * ARG (BUILD A *X R IN 0 MEETING))) (M8) 50 MSECS *(BUILD HEM GABOR CLASS PROFESSOR)

**;Pat is a professor. *(BUILD HEM PAT CLASS PROFESSOR) (M9) 10 MSECS **;Gabor is a professor. (MlO) 8 MSECS **;Nick is a professor. *(BUILD MEM NICK CLASS PROFESSOR) (Mll) 8 MSECS **;John is a professor. *(BUILD HEM JOHN CLASS PROFESSOR) (M12) 8 MSECS **;Stu is a professor. *(BUILD HEM STU CLASS PROFESSOR)

(Ml3) 9 MSECS ~~;Pat is in the hall. *(BUILD A PAT R IN 0 HALL) (Ml4) 11 MSECS **;Nick is in the hall. ~~(BUILD A NICK R IN 0 HALL) (M15) 10 MSECS ~~;Who is in the meeting? *(DESCRIBE (DEDUCE A i~ R IN 0 MEETING)) (M17 (MIN(O)) (MAX(O)) (ARG(M16))) (M16 (A(PAT)) (R(IN)) (O(MEETING))) ; Pat is not in the meeting. (Ml9 (MIN(O)) (MAX(O)) (ARG(M18))) (Ml8 (A(NICK)) (R(IN)) (O(MEETING))) ; Nick is not in the meeting. (M20 (A(GABOR)) (R(IN)) (O(MEETING))) ; Gabor is in the meeting. (M21 (A(JOHN)) (R(IN)) (O(MEETING))) ; John is in the meeting. (M22 (A(STU)) (R(IN)) (O(MEETING))) ; Stu is in the meeting. (DUMPED) 1427 MSECS 7.3 Example 3 We assert that between two and four dog owner­ ship relations involve spoiling, and assert four such spoiling relations. SNePS deduces that Jim does not spoil Lassie. **;Of 5 dog ownership relations, * ; b~tween 2 and 4 involve spoiling. ~'<; 5:il2x,y [}iember(x, person) ,Member(y, dog), *; Owns(x,y) : Spoils(x,y)] *(BUILD ETOT 5 EMIN 2 EMAX 4 PEVB($X $Y) * &ANT ((BUILD MEM *X CL4SS PERSON) * (BUILD MEM *Y CLASS DOG) * (BUILD A *X R OWNS 0 *Y)) * CQ (BUILD A *X R SPOILS 0 *Y)) (M5) 81 MSECS **;John is a person. *(BUILD MEM JOHN CLASS PERSON) (M6) 10 MSECS ~'< ; Jane is a person. *(BUILD MEM JANE CLASS PERSON) (M7) . 10 MSECS **;Mary is a person. *(BUILD MEM MARY CLASS PERSON) (M8) 9 MSECS ~~;Jim is a person. *(BUILD MEM JIM CLASS PERSON) (M9) 9 MSECS **;Rover is a dog.

~'<(BUILD MEM ROVER CLASS DOG) (MlO) 9 MSECS **;Spot is a dog. *(BUILD MEM SPOT CLASS DOG) (M11) 12 MSECS **;Lassie is a dog. *(BUILD MEM LASSIE CLASS DOG) (Ml2) 10 MSECS **;John owns Rover. *(BUILD A JOHN R OWNS 0 ROVER) (M13) 11 MSECS ~'<;John owns Spot. *(BUILD A JOHN R OWNS 0 SPOT) (Ml4) 11 MSECS **;Mary owns Lassie. *(BUILD A MARY R OWNS 0 LASSIE) (M15) 13 MSECS **;Jane owns Spot. *(BUILD A JANE R OWNS 0 SPOT) (Ml6) 11 MSECS **;Jim owns Lassie. *(BUILD A JIM R OWNS 0 LASSIE) (M17) 12 MSECS **;John spoils Rover. *(BUILD A JOHN R SPOILS 0 ROVER) (M18) 10 MSECS **;John spoils Spot. *(BUILD A JOHN R SPOILS 0 SPOT) (Ml9) 12 MSECS **;Jane spoils Spot. *(BUILD A JANE R SPOILS 0 SPOT) (M20) 12 MSECS **;Mary spoils Lassie . *(BUILD A MARY R SPOILS 0 LASSIE) (M21) 11 MSECS **;Who spoils whom? *(DESCRIBE (DEDUCE A i~ R SPOILS 0 %Y)) (Ml8 (A(JOHN)) (R(SPOILS)) (O(ROVER))) ;John spoils Rover. (Ml9 (A(JOHN)) (R(SPOILS)) (O(SPOT))) ;John spoils Spot . (M20 (A(JANE)) (R(SPOILS)) (O(SPOT))) ;Jane spoils Spot. (M21 (A(MARY)) (R(SPOILS)) (O(LASSIE))) ;Mary spoils Lassie . (M23 (MIN(O)) (MAX(O)) (ARG(M22))) (M22 (A(JIM)) (R(SPOILS)) (O(LASSIE))) ~J~m does not spoil Lassie. (DUMP~DJ 1341 MSECS

8 . SUMMARY

We have discussed the roles of existential and numerical quantifiers in reasoning programs. The roles are different and both are important. The existential quantifier is most useful for supply­ ing referents for designating phrases with no previously explicitly mentioned referent. Numeri­ cally quantified rules are concise representa­ tions of rules that govern reasoning by the process of elimination and can introduce ex­ plicit negatives into a data base or can use negative statements for deriving positive state­ ments. The most general schema for numerical qu~ntifiers that we have discussed is n~{X(Pl(x), .·. ,Pk(i):Q(i)), which says that at least i and at most j of the n sequences of individuals that satisfy P1(:K)& .·· &Pk(x) also satisfy Q(X). We showed how rules of this form can be represented in SNePS, the Semantic Network Processing System, and gave examples of SNePS runs that used such rules for carrying out inferences.

Two aspects of numerical quantifiers might limit their immediate usefulness. One is then parameter, required whenever the minimal para­ meter is present. In formulating numerically quantified statements, we have found specifying n to be bothersome. The parameter could be eliminated if the inference system had another means of determining how many individuals satisfy the restriction, for example if the closed world assumption held. The other problem is that inherent in any counting argument is the assumption that any two individuals are, in fact, distinct. If this assumption does not hold, the use of numerical quantifiers depends on a solution to the identity problem mentioned in Sec. 3. Except for these two problems, numeri­ cal quantifiers seem to be useful additions to the tool kit of representation and inference.

ACKNOWLEDGEMENTS

The author is grateful to Don McKay for help in SNePS development and to him and Rich Fritzson for SNePS and Lisp system support. He is also grateful to Brian Funt and Don McKay for comments on an earlier draft.