A Many-Sorted Resolution Based on an Extension of a First-Order Language

1. Introductjon

Within the field of theorem proving, the advantages of a many-sorted logic are weil known (Hensehen, 1972 and Cohn, 1983]. More recently a sound theoretical foundation for many-sorted resolution has been established in [Walther, 1983, 1984a] and the power of a many-sorted resolution has been demonstrated by an example in [Walther, 1984b]. However, because of its associated fixed structure, sometimes not as much advantage can be derived from the use of a many-sorted calculus as one would like to get. This is illustrated by the following example.

Example 1.1 Let :r, , :r1 , :r, , zd , and :r, be the vari­ ables rapging over the sorts A , B , C , D , and E , respectively, where D C B , D C C , E CA , E C B , and E C C . Suppose the theory to be refuted is given by:

1. V:r, Y:r1 (P (:r.) U Q (:rt , fd (:r.)) UR (:r, , :r.)),
2. V:r, ..., P(:r,),
3. V:r, V:r, ..., Q(:r,, z,),
4. V:r, ..., R (g' (:r,), :r,),

where fd(:r.) and g'(:r,) are Skolem functions whose ranges are restricted to D and E, respectively. Suppose (1) and (2) are resolved,"because :r1 of P(:r.) in (1) and :r, of ..., P(:r,) in (2) are unifiable over D. The two elauses can be resolved using the mostgenerat unifier (mgn) 8 = {IId /z1 , IId /z,} where IId ranges over D . The deduction is then

1. Q (IId , fd (IId)) UR (:r, , IId) (1)+(2)'
2. Q (IId , fd (IId )) (4)+(5) .

It is noticed that (6) eannot be resolved with any other clauses, not even with (3) because no sort is known to be a subsort of D arid E . A dead end has been reached. (5) is a useless resolvent, so is (6).

·Thia work was oupported in part by Air Force Office Scientific Resea.rch under contra.ct F41111~82-C-0089.

Had there been another sort G ""' B n C , :r1 of P (:r1) in (1) and :r, of ..., P(:r,) in (2) could have been unified over the sort G giving the deduction

where 11 1 ranges over G · The clause (6 1 ) can be further resolved with (3) resulting in the empty clause 0. There is no dead end here. It is observed that the need for G is not known until (1) and (2) are attempted to be resolved. In an ordinary many-sorted langnage, one cannot add a new sort whenever a need arises without altering the sort structure.

To alleviate such a situation, an extension of a one-sorted language called one-1orted langutJge witla aggregtJte tJBriBblel ( L r! ) is proposed into w hieb a many-sorted theory can be translated and which may be dynamically extended to bypass the problern illustrated above. Previously in (Shin and Irani, 1984], the concept of embedding aggregatevariables (a.v.) into a many-sorted language (L .. ) was reported, and its resulting langnage was called manJI"10rted language witla a.tJ. . Here a.v.'s are embedded in a one-sorted langnage.

a.v.'s allow the introduction of range-restricted variables dynamically without revising the a priori fixed structure. Using the dynamic range-restricting nature of an a.v., an effi­ cient many-sorted resolution scheme called UWR-re10lution is presented which is designed to avoid generating useless resolvents as illustrated in the above example. The complete­ ness of UWR-resolution can be shown. The efficiency of UWR-resolution is discussed.

2. One-IQrted L&QIU&Ie wjth ·· y. L t

:1.1. Syntax of Id

In L~ two types of variables, called simple variables and a.v.'s, are available. A simple variable of ~ is the same as the ordinary variable of one-sorted language. Unlike a simple variable, an a.v. is syntactically an ordinary sort variable, but semantically a variable whose range of interpretation is res­ tricted by a unary relation rather than to a sort universe. Formally stated, an a. v. is of the form :rEP' in which :rEP' ranges over the unary relation indicated by the unary predi­ cate symbol P, .

Let J , L , and K be respeetively a relation index set, a function index set and a constant index set. In addition, Iet I be an index set for some unary relations. Let >. and € be functions such that >.: J -+ N+ and €: L ..... N+, where N+ is the set of positive integers.

Definition 2.1 A one-1orted language witla tJ.tJ. ~ then consists of the following : (1) parentheses (, ) and a symbol E ;

(2) constant symbol Ct , for each k E K ; (3) simple variables d , u u, r x 1 , · · · , Xm , · · · , an a. v. s z 1 ' , · · · , z,. , · · · , or each i EI , where P, is a unary predicate symbol; (4) a >.(j)-ary predicate symbol R 1 , for each j E J ; (5) a {(I )-ary function symbol F1 , for each I E L ; (6) logical connectives , , and -+ ; and (7) a universal quantifier V.

Based on this language, the lerm· of ~ are defined as usual except that each variable is now either a simple variable or an a.v .. The set, Form(Lt), of well-formed formulu of L~ , is defined as usual. The definable syntactic objects u , n , !:+ and ::::1, and the standard notions such as ·en­ lencea are also introduced in the usual way.

2.2. Interpretation of L-1

A structure is needed to interpret each formula in ~ . Let os. be a structure for L~ . Then OSa = < 0, {P, }oEI , {R~ }; EI , {F, }tEL , { Ct hEK >* where o is the universe or os. ; ?, is a unary relation ?, ~ o ; R~ is a >.(j )-ary relation R~ ~ o'(J) ; F, is a {(I )-ary func­ tion F 1 : 0~ 1 > -+ 0 ; and a distinguished element Ct is an ele­ ment of 0 , for each k E K . The interpretation of a formula in the structure os. then requires a variable assignment runction 8 as follows:

Definition 2.2 For a set V of variables of ~ and the universe 0 or structure os. ' 8 is an assignment function 8 : V -+ 0 such that for a simple variable z , 8 (z) = a , w here a E 11 ; and for an aggregate variable

Assignment function for the terms of ~ is defined as usual. For notational convenience symbol 8 is also used for the assignment for the terms. The validity of each formula is determined by the following interpretation rules.

Definition 2.3 For R 1 (1o, ... ,l >.(;)), .,1 ,Y,2 EForm(L~), where I, 's are terms, the satisfaction of the formulas with respect to 8 in os. is defined by,

1. I=; R 1 (1 0, · ·· , 1>.(;))[8] iff <·(1 0), ··· , ·(l>.(f))>ER 1 , os,

1. I=; 1/11 -+ .P2Is] irr if I=; 1/11[8] then I=; Y,2[8] , ~ ~ ~
2. For a simple variable z , I==; Yz Y,1 [8] irr for any os, a E 0 , Fbs 1/11 [8 (z I a )j ,
3. ( 5) For an aggreg~te variable z EI', , 1-- Yz EI', Y, 1 [s] irr for l"""""ös, . EI' any a E P, , I==; 1/11 [ 8 ( z ' [ a )] os,

w here for variables

11., and

As a corollary to the definition, the interpretations of U , n , !:+ and ::::1 can also be easily defined.

2.3. E-Extensibility of U

L~ is as convenient as L., in abbreviating the relativ­ ized expressions in a one-sorted language into more compact forms . Jf a formula u., m L., is of the form

· From next section on, " · " on a symbol is omitted ae: Ion« as the meaning of the symbol is unambiguous.

w here z, is a sort variable betonging to some sort S, , then u,. can be syntactically translated into ur_ in L~

w here the unary relation intended by P, is identical to the sort S, . During the translation, ~ is augmented with P, and accordingly the structure for ~, say OS. (Lr. 1 )' , can be constructed from the many-sorted structure for L., , say MS (L,.) . The following theorem can be shown (proofs for the theorems given in this paper can be found in (Shin, 1985]):

Theorem 2.1 A sentence u., in L,. is true in MS(L.,) irr ur_ in ~ is true in os. (L r. 1 )' ·

The power of ~ over L,. lies in the fact that w hereas in the latter a sort variable with new sort may not be introduced, in the former a variable who1e rangt i1 re·tricted to 11 1ub·et of the univeru 0 can be introduced a· needed in it1 ezlen­ ·ion. Let TE be a theory in . L~ and Iet a formula ~ E TE be or the form

In L~ , in order to introduce a variable ranging over S 1 n S 2 , all that must be done is to add a new unary predicate symbol St to L~ , abbreviate ~E by Vz r.s, 1/!(z r.s,) , and augment TE by the defining axiom Vz ( S.{z) !:+ SIIz) n S~z)). The extended language L~' is called a E-ezlen8ion of ~ and the augmented tbeory T r.' , a !;-ezten8ion of T r. . For the semantics of the new predicate symbols in L ~ ' , it can be shown that there is a unique expansion by definition or os. ' say os. 1 , which is a model of Tr.' . os. 1 is called an ezpamion by E- definilion of os. . This characteristic of ~ is called E-eztenaibility. The following theorem establishes the validity of E-extensibility of ~ :

Theorem 2.2 that for Fas· 1/1 1 [s] . For any 1/1 1 E Tr.' , there is a 1/1 E T r. such any assignment function 8 , <=> I=; 1/1 [s ]. os,

3. UWR-resolution

The problem identified in Section 1, namely, the genera­ tion of useless resolvents that Iead to dead ends, occurs only w hen a many-sorted theory of a certain class is refuted by a resolution scheme. For instance, for the many-s<irted theories with tree structure stated in (Walther, 1984a], this problem never occurs. When the tree constraint is lifted, however, this problem may appear. The conditions under which the prob­ lem may arise are explained below, this time in terms of L t .

Let Ran (I) stand for the range associated with a term I . Given a set of unary relations P , Iet a set of immediate predecessor of a relation P, E P , denoted by IM(P,), be d defined by IM(P,) = {P 1 I P 1 E P , P 1 C P, , and if P 1 ~ P1 ~ P, then either P 1 = P1 or P1 = P, }. A situa­ tion may occur in which two variables 11, and 11 1 have I IM (Ran ( II, )) n IM (Ran ( IIJ)) I > 1 . Hence there are possibly more than one range over which 11, can be unified with 11 1 · In fact, if Zt is a variable such that Ran (zt) = Pt and Pt E IM(Ran (11,)) n IM(Ran lv;)), then any substitution e = { zt/111 , zt/11 1 } is a legitimate mgu of { 11, , 11 1 } , since 011, = 811 1 · There are, therefore, as many mgus for

{ v,, v 1 } as IIM(Ran(v,))n/M(Ran(11 1 ))1. Notall the resotvents generated using each of these mgus are useful.

A way to remedy the situation is proposed in the follow­ ing. First, a few new notions are introduced. A wr­ ·ub.titution component is any expression o( the form tfv , w here v is a variable and t is a term different from v satisfying Ran (I)~ Ran (v). A wr-1ubpair is a set o( wrsubstitution components {1/v, , tfv 1 } satisfying, (1) Ran(v,)(j Ran(v 1 ) and Ran(v 1 )(j Ran(v,), {2) I IM (Ran (v, )) n IM(Ran (vl)) I > 1 I and {3) Ran (I)= Ran(v,)nRan(v 1 ) . A wr-·ub1titution is a set o( wr­ substitution components which possibly contains one or more wr-subpairs. A wr-re1olvent is aresolvent which is generated by using a wr-substitution as a unifier.

The E~xtensibility o( ~ plays the central roJe in intro­ ducing wr-subpairs. From the definition of a wr-subpair, it is clear that wr-resolvents can only be expressed in an extended language o( Li . To be more specific, Iet a theory in ~ be formalized by an ordered pair < OA , Tr; > where OA is a set of ordering axioms expressed with the symbol " C " such that P, C P 1 means Yz ( P,(z)-+ P 1 (z)) and Tr; is a set o( the nonlogical axioms of the theory expressed in Lt . The following is an example:

Example 3,1 Consider the following < OA , Tr; > :

• OA : {1) D C B , D C C
• E C B, E C C

The following is done: For zi:B of P (zi:B) in (3) and zEC o( -. P (zr;c) in {4), a wr-subpair { z'EK /zi:B , z'EK /zr;c} is introduced with Lt being extended by a unary predicate symbol, say K, where Vz {K(z):OB(z)nC{:r)). The extension of Li requires < OA , T r; > to be also extended, i.e., OA is augmented to OA + by the ordering axioms such as (2+) below. (6) is derived as the wr-resolvent of (3) and (4). Finally, (6) is resolved with (5) resulting in 0 as follows:

It is not difficult to see that the range of I in a wr­ subpair {1/v, , tfv 1 }, i.e., Ran (I)""" Ran (v,) n Ran (v 1 ), is the weakest range over which { v, , 11 1 } ean be unified -­ weakest in the sense that if P." ... Ran (I), then there is no P1 such that P." C P1 and 11, and 11 1 are still unifiable over P1 · For this reason, the unifieation stated above is ealled unification over the weake·t ranse and the resolu­ tion involving such unification is ealled UWR-reeolutlon. The idea behind UWR-resolution is therefore to subsume all the possible unifieations by one unifieation over the weakest possible range.

The eompleteness of UWR-resolution must be proved. Given < OA , T r; > , Iet Rw ( T d be the set o( all clauses consisting o( memben of Tr; and the resolvents (including wr-resolvents) of memben of Tr; (similar to Robinson's reso­ lution operator (Robinson, 1965]). Also Iet R.;,(Tr;) be defined so that for each n ~ 0, R.2(Tr;)- Tr; and R.;,+ 1 (T:cl- Rw(R.;.(Tr;)). Completeness theorem states:

Theorem 3.1 A < OA , Tr; > is unsatisfiable if and only if Rif(Tr;) contains 0, for some n ~ 0.

In fact, when the UWR-resolution IS applied, < OA , Tr; > is refuted not in Li but in its extended language Lt' . Therefore it further must be justified that w hen R if ( T r;) contains 0, for some n ~ 0 , w hether the unsatisfiability of < OA , T r; > can be truly shown in Lt without extending its vocabulary. Let RJ.. ·) stand for an identical situation as Rw ( ·· )· except that in the former no wr-resolvents are generated. In this way the unsatisfiability of < OA , Tr; > can be shown without extending Lt. The following theorem can be shown:

Theorem 3,2 Given < OA , TE > , R; ( T r;) contains D, for some n ~ 0 , if and only if R ~ ( T r;) contains 0, for some m ~ 0.

4. Efficiency of VWR-resolutjon

One way to discuss the efficiency o( UWR-resolution is to com pare R w ( · ) and R J.. · ) defined previously. The fol­ lowing facts show the efficiency o( UWR-resolution:

Lemma 4,1 Given < OA , Tr; > , if n is the smallest non-negative integer for which R/f(Tr;) eontains 0 and m is the smallest non-negative integer for which R r;'" ( T r;) con­ tains 0, then n = m .

Lemma 4.2 Given < OA , Tr; > , for each ~0 1 RI/ 1 (Tr;)- R/v(Tr;) 1 ~ 1 Rl:+l (rr;)- Rl::(Tr;) 1

Finally, the following theorem ean be proved:

Theorem 4.3 Given < OA , Tr; > , if n is the smallest non-negative integer for which Rif(Tr;) and RI:(Tr;) both contain 0, then I Rif(Tr;) I~ I RI:(Tr;) I·

5. Conclus!on

The use of aggregate variables have been demonstrated in a new approach, namely, UWR-resolution, for proving theorems. It has been shown how such an approach avoids the problems eneountered in the use of a many-sorted language.