A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation

1. IAirOductjqo

Tbe advantaaes ct a many-101"\ed calcvJus in automa\ed reasonina systems are well known [Hay71, Hen72, Wa33, GMS-4, GM85, Co83, CD83, Ob62] . a fact tb1t was also not.iced in .lQiica1 progr1mming [MOM, MiM]:

In a many-sorted calcuJus we obtain 1 sbclrter refutation of a smaUer set ct lbq1er clauses. u compared to tbe unsorted verlioft.

Our interest is in using a many 1011ed calculus ill Autoaalted Theorem Proviq, npecia.Uy in resolutiofl based ATP-systems. Tbe most desirable properties ct sucb 1 calcWus are:

• 1.) The un10tted probJemand tbe oorresponding sorted problem are equivalent, ie. tbe unsorted cl1use set is contradidory, iff tbe sorted version is
• contradictory.
• 2.) Tbe caJcuJus is complete, i.e. tbere is a derivltioo of tbe empty clause, iff tbe cl1use set is contradictory.

Some IU\bora pretent sort struc:tutet, IUCb th1t tbe unioG, tbe intersec:üon and the c:omplement d sorts ar. dlfiDtd [Co83, CD83]. II aucb .iatorm1ticla ia used in 1 dlducüon, tbe ruJes d t.be :tRP--calculuslte not sufJ'idnt and ent1 ru»a wOU1d be DIOIIIU'Y to euure coapletneaa. But -* nva ru»a bave in antral tbe very UApjeiiiDt Iide tlfect tbat 1.be reductJcea lad IU'Iteaies d a resolution b1sed

for tvo polymorphic: terms is alw1ys finite. c:aJculua are DO .lolailer lfPÜCible.

2. Baaic NotiQQI c( 1.bt ERP·-calcu&us.

In t.be fol.lawiJal ve apecify tbe UAderlyißt kllic­ Tbe DOll stllldltd Pll'1 d 1.be Dllt defauliona are t.be po&yaorpbk fuftC.'IäoDa. Ye aujp to every fww:Uon the Mt d aU doaliA-ranae relaliooa, e.a. ror tbe aum

( +) d coapleJ auabera ve bave:

• : OOMPLEX · OOMPLBX-. OOMPLEX ; OOMPLBX · JNT -. C0MPL11 ; INT · INT -. INT ; ...

Tbis il . deDo&ed IS I set ol triplea {(COMPLII,OOMPLEX,CONPLEX), (I NT ,JNT,INT ),

(OOMPLBI,INT,OOMPLBX), . . J.

Defipjtjq) · A oatymarobic Wpature SIG is a triple (S,f,), vhere

• 1 ) S ia the finite set ol sorts, s ia 1 plttiaJ orderina oo S with the atel1ell element T. s ia eJtendtd to
• tupJea d sorta iD 1.be uauaJ v1y {c:ompoeentvise s).
• P is the set ol functioo symbola. P .. U Pw , where Fw is tbe set ol function symbola ol arity n vith

lf Pw ,. 0 , tben W 11tillie1 the foUowiDa

• m .. w ~sn·1 condiüoos:
• The tort or constants is unique. i.e. W' S impliea
• IWI · 1.
• For lianatures ol functiona W, vhicb are not
• CQQitant:
• W contaios a unique are1test element <sw.t.SW,2·· · · .sw .n· 1 >.
• For every (S 1 , s 2 , .. . . s 0 · 1 ) E W and every (T1···.Tn) E Sn, (Tt····,Tn) s (St·····Sn) implies that tbere eiiats 1 unique JOrt T D+ 1 s Sn+ 1 auch tbat (Tl· . .. ,T n+ l) E W. Tblt mellll tbat ror every r E P the rela&ed runction r· : ((S1 ... ~ .S 0 ) I (St , ... .Sn) s ($w 1····.5w 0 »-. S, ' ' vbere r·(s 1 , ... .Sn) ·Sn+ 1 , ilf (5 1 , ... .Sn+ 1 ) E W, il vell defioed ud moaotooe.
• P i1 tbe Mt d predicate symbols. If PD il the set ol precücl1el With domain D, Tibete D E sn. We def'iDe P · V J1n.
• ·0 Pot every 10ft S E S, there eliats a coostant c ot tort S' ~ S. Tbat aeua, tbat SIG is strict in tbe MDied[BOIO],

We uae tbe foUowina addit.ionaJ notat.ion and lltbrevi1tioDI: SO(t) · Y. ilr I E Pw; SO(P) · V, i1T P 1 Pv. C deoocet the set d 111 c:onstlllts, Cs denotes tbe set ol 111 ooostanu d 10ft S.

lf 1he tel d ranaet ol I functioo C, i.e. tbe set tsn+ 1 Ms 1 , ... .Sn+ 1 ) E SO(t)t Iw mcn Uwa one elelllent, tbea r il called a DOlymgrpllic func:Wn. Ir 00

polyaorpbk fuacüoft ia ~ P, lbn SIG ootretpODda to a aipalure d tbe ERP-calculua [W'a83l

In aa IClual iapleaentatiorl, it il not MCelllfY, tbat tbe vbole lipalure oC a fuac:tioo ia tipücilely spec:ified. lt il aulricient to aiV· eoouall iDCormation to coapute tbe lianlture d 1 CUQc:tioo uniquely. For fuftCtioel, vbidl are not polymorphic, tbe spec:i(ic:at.ion d tbe mu.imal domain and mu.imaJ

raaee lufl'icta.

Let Y 5 be tbe (infinite) tel ol varilbles ollOft S and

Iet f · Vt 5 . Terms (i1M:ludina ill-IOfted terms) are

defiMd u uaual. Tbe set ol 111 terms is ca11ed TERM. Tbe 10ft d t , namely [t] , is defioed 1s Collovs:

Tbe ruoc:lioll ( .. J maps ooostants and vwiables to their respective torts and is recurl.ively extended to terms by [f( t 1 ·····'n )] · Sn+ 1, i1T Si · [t~ and

(S 1 , ... ,5 0 + 1) E SO(f). Wt defioe ETERM, tbe tet ol all

veU-I(Illd wms u the domain ol the runction [... 1. i.e. tbe was, ror vhidl1 sort is defined.

The func:tional refteJivity uioma are the uioms 'VI I · I, IDd ~~ l····.Jn f(I 1 , ... ,In) · f(I 1, ... ,ln).

EumDJt. lAt S · {N, Nl, 7J, vbere N denoles the nODMtative inteaera, i1M:ludina 0, NZ denotes the positive iotetera and Z · {0}. Tben Na NZ and N ~ Z. Tbe fuac:tioll + Iw tbe follovina aianature:

SO(+) · {(N,N,N); (N,NZ.NZ); (NZ,N,NZ); (l,N,N); (N,l,N); (Z,NZ,NZ); (NZ,Z,N'l); (Z,U); (NZ,NZ,NZ) }.

Then for eumpJe [0+0] - Z and [0+ 1] · NZ.

DellAi\ion~ Por 1 aiven sJ&oature SIG · {S.f.P) we s1y tbe ltipll {A,S.f) il ao tiRtbt· ct tyoe (U). if tbe faüawioa il aaüsl'ied:

• A ia 1 AOOempty aet.
• To every IOI't S E S il atliped a aubset sA d A lucb tbll TA · A Ud fot an s.T ES: s s T · sA .a tA.
• Pot c t (s. 1D ellmeat cÄ E A eiiltl, tucb tbat cÄtsA.
• For runcüoftt f. rA: A0 .. A. 11 1 mappifta suctl t.bat the iaqe d s 1 A x !II x Sn A it in Sn. 1 A for al1 {S 1 · I ·· ,s 0 · 1 ) t SO((). 0

By U. detiait.ioe d 1 lipatute, we bave tbat sA ,. II for every S 1 S liaoe every tott cootlins at Jeut 061 coostaat.

DefiAiJ.oA. A a1ppiq ' : A .. B · wbidl hu 1.be propetÜII, lbat

1. ·<sA) s t<S 8 ) ror ~ 1ott s es Md
2. ,uA<a1 .. .. . ~n> · r8<t<·a > ... ···<~n))

iscalled a E · JMUPO'MDN'·· 0

{ETBIM.SI) il tM froe .... btl ct type (SI) aod (!:TBRMer.SI) it SM inlUil llaebrl d type {S,J), wbere ETBKMar it t.lle ·t clterlftl witiMMit v·ilblet.

A aappiaa e: ETDM .. ETDM, whidl is 1 E -endoaorp.bism wlllte (l t V I ex .. I) il finite, il caüect I E -qbllityli<& Le\ ESUB be .... .., d a1J E-subltüWoDI. E-tubllitu..-. ·· e1ec:&ly tboae aappiaat. wbicb are tubttitutioet in tbe normal sense lAd have tbe additiollal property that

[4ftdh (JJ ror alllt f.

P(tl· .. ··'n) il an IIWil. wbere P ia a predicate syaboJ and tbe t 1 ·a are wraa auch tbat l't) $ s 1 Where

(Sl .... .S0 ) · SO(P). A .. WitllJ.t I tillled 1to11. A GIIUil

il I set ct litetllt, i.t. lA lbbreviatioD fot tbe diJjuncUon d tbe Werall, wbere al1 variables are univerlllly quaa\itied~ A uCHIIld &tom. 1 uound w.tal or a lfOUAd dau· ia oee without v·iables. IQ!llpqe d atoaa, liwrall aad dauaet are their i .... t under a E-tubtütuUoe. lklullit.y (·) is a diltiftauilbed bifllry predicate witb doaainlottl SO(·) · (T,T).

Since a ctau· aet es illaid tobe aatilf'ilble, if aad onty if 1 aodel ror es tliltt, &bete i1 t.he neec1 ror a precile definitioD d a model r"pec:t.iaa polyaorphic sip1tures.

lllfioi\QO. A EE-modlt for I daUM aet a il 1 ltiple (D,SIG,R), wbicb satilfiet tbe followina conditioat:

• (D,S,P) is an aJsebra d type (S,f).
• for every predk:ate P tbere eliltl a relation pD E R ct the aame arity.
• All clause1 in es tre vaüd under al1 E -homoaorpbilmt ': ETBIM -. D, i.e. al1 clau·· 1te valid uader al1 usjpmeels d values in D to variables in c:lauses, wbere lotts are respected. (A liWal +P(. .. ) il vaüd under ·· if it's imqe undlr' il in t.be relatioll pD)I
• Tbe equaüty predi<:aw il represenwd u t.be identity on D.

3.Upifigtm oC Potymorphic Terms.

For 0 E ESUB we UM the notatioo:

DOM(o) ·(I E VI ox .. 1); OOD(o) ·(eil I E DOM(o)} aad vooo (e) is tbe set d variable· in COD(e). A udkaüoo problem ror two terms s and t il denoted u <t · t>. The Mt d variabiet da term t il deooted aa VAl(\).

Por W !ii Y aod o;c E ESUB, deliDe 0 · t' (WJ, iff ex · t1 ror ll11 E W. Purt.beraore deliDe e !ii t' (W]. ;rr o · At' IWJ for soae A t ESUB. Obvioully !ii IWJ is 1 relle1ive aod ltaaaitiVe reJation oo E -subatitutioos. Pot a aubaet U ; ESUB we aay U is separated on a aet d VM'iablls W, iff DOM(e) · W llld VCOD(e) n W · 16 for alle EU lßd al1 VOOO't art disjoint. NoC.e \hat tucb a set aaaittl d idempotent E-substitutiool only.

Dlfjnitjqo. A set ct mott aeoeral Wlifiers JIUE(s,t) for two terma s aad t is defined u 1 subaet oC ESUB, which it aeparated on W · V AlUs,t) aad satilfies:

• css · 45\ Cot al1 0 E JIUE(s,t)~ (oorrectness).
• For 1116 E ESUB witb 61 · 6t we have 6 !ii e (W] for soae o E Jltl:(s,t). (c:ompleteMII)
• e S t' (WJ .. e · t' for al1 eJ,t' E JIUE(s,t)_ ( ainiaaüty) 0

IWipiüop. A E -Substitution is 1 nattgjps tubiÜtUÜOQ (COifdaa) (Wd.f,GMISl. iff

• (i) e aubttitutet vitiabitt ror variabln aad
• (ü) · il injec:Uve oa DOM (e) ud

(iü) DOM(e) n VOOO (e) ··~ 0

TM ·· d a11 weaktDilaa subatitutioos il called EYSlJB. ln tbe coaputatioG d a set d aott aenerat unifilra, weakenifla aubltiluüoos are uaed 10 IOive uaifi&:aUaD problemslitt <X · t> , wbln [t) ia DOt a lublotl d [J].

fWiaitjgO Tbe set ct AlOit ..-11 nektpjps ·MI&itmm· tw t lAd s. JAWEsh) is a tet d

weateama aubstitUüou whicb il aeparated oa W · VAI(t) llld u&ilfiet:

• [e1.] s s rot 111 e E )1\VEs(t). (correaness)
• ~ E !:SUB with [&1.) s s tbere e1ilta 1 e E )1wt 5 (t) such thlt & Ii e (W). (compieteMU)
• "e,'C E )lftgh): e Ii 'C [W] ~ e · 'C. (ml.nlmllity) 0

Tbis defiailion 11 ot coutH oely ullt'ul rot terms . wbich are W-sotted ot fot terms t where [1.] il not 1 tub10ft ot s and tbe ou1erm01t fuDCtioa symbol ot t is polymotpbic.

The followina lheorem is vaüd in tbe !:RP-calculus [\VII3,\VIA.fl and ca be tJtended toERP·.

Ihtq'em L [Sch85a]. LettE TBRM and SES. 1f tbtre uists 1 8 E ESUB such that [8tJ s s. then )1\VEsh) uists, it 11 not empty and it il atw1ys finite.

An immediate coa.sequence il:

Theorem 2. Pot UD.itiabie I Ud t the set )I.UI:(I,t) nista, is not empty and fiaite. 0

The proor follovs rrom tbe fact ,that )I.UI:(I,t) ·

(t!Je(J t- et) I es E )l'WE[Jt)), if 14 V Al(t).

Bnmole. The followina tllllPlt dtmoaslrltes, tbat fot 1 unificaüon probaem <l·t> the minimal Mt ot most aeneral unifiers ca arow tlpooentiiUy.

Contider tbe sort slructure S · {N,NZ,Z), where N, NZ and Z have tbe 11me meanina 11 in tbe e11mple above. Let I E YNZ ud Ii E YN. The sipature ot the function ..... (ptoduct) il:

SO(·) · {(N,N,N), (NZ,N,N). (N,NZ,N), (Z,N,Z), (N,Zl), (Z,NZ,Z), (NZ,Z,Z), (Z,Z.Z), (NZ,NZ,NZ)}. The unificaüon probte· <I · (11+12>- ... ·<t 20 _ 1 +Izn)> produces 2° unifiers, liDce fot every · fiCtor there are two independellt solutions ( 1 21 _ 1 ... Yzi-1} 1nd (Izi .,_ y 2 i>. where [y;l · NZ. These solutioas h1ve tobe combined indtpelldtllUy.

Fot 1 set d variables \V ud 1 aet ot E -aubstituüons U, the 11t MAX;[W]CU) is a tel ot E-tubsütutiollls , suchtbat

1. MAXsa:wJU) ~ U and
2. Ii) ""E MAXslwJCU). 'CE U: e Ii 'C (W) ~ e · 'C.
3. iü)"" E U: 35 E MAXsfwjU): t' Ii e (\V).

Such a ltt ttista, since li(W) islriJllitive.

The polymotpbic unifk:atJ.oll lltotitha !:VNIFJ. whlch is lll eltensioa ot tbe aJaotitha rot the ERP-caJculus [Wd.f), tat" two tetas s,t as illput 1nd produces 1 Iet ot a01t ..-rat unif.i.ers as output. lt is defined II follows: (Sdl85a]

1. UNEW · {d.
2. RBPBAT UOLD : ~ UNBW· UNBW · 0.

Fot every e t UOLD 00

Let (d,e) bt the fit" ditqrHaent pair ol the wo teta· esa, cn.

IP d ot e is 1 variable, TRBN 00

UN!W· U~ I~ E )I.UJ:(d, e)t .

00.

00.

UNTIL UNBW is I set ot 1:-udierl fot s,t or

UND'" 8.

1. RBTURN MAX; [VAR(s,t)) (UNBW ). 0

We havt tht t.beotem. wbich is proved in (Scb8~1): Tlltorta 3. Let s,t E EIIRM bt 1:-UD.itlablt. Then EUNIPY(I,t) tetmillllel md retumt a finite ftCGtapty llt, vhich is equiValent to JJUJ:(s,t). 0 DICioitim Wt say SIG is 1 upU1qt!oo unigue stan1ture. ur

• < S.s > is 1 11mil1ttiee witb 1 uniqut are1test tlelltftl.
• For 111 r E P md 111 s E s. tbe set {(S t ·····Sn+ 1) E SO(f) I Sn+ 1 s S} is either empty or

OOGI.IAAa 1 ullique areatest elemnt.

Tbe followillalheorem is proved in [Scb85al. Theq'tm i. Let SIG be 1 uiUfic:ation unique sign1ture. Tben )I.UI:(a,t) is 1t m01t 1 ainaltton for 111 s.t E ETBRM. 0

lll (Scb85al it is sbown, that the OOGdition, lhlt < S.s > is a ~tailatlice, doel not l'fltrict tbe tlpressiveness ot the aoy-lotted calculus tRP·. Jn the cue that <l,s > it 1 Pltlially ordered tet, it is poslibie to add IOfll to the sipl&urt, auch that tbe resuJtina 1ott slructure is 1 11milani<:e md tht Slt.itriabilty ol

dau11 aeu i· ullcbuaed.

of. Tht tRP· -gk;ulus.

E -ractorilltiOD, !: -retolution and !: -par1aodulatioo .. defined 11 in [WIA31. .bowever b11td Oll tbe uail'ier 11ta JJUI: ud t~PE reapecüvety. Tbe 11t JIP'E il the set ot most &elleral unifiert for para­ modulation, whic:h is aleo att11ya finite. The 1:-patlmodulltioa rule indudes tbe weakfllina ruJe ot [\Val3] . Tbe prooft iJl [\VR73] can be generalized (Me [Scb85a]) U> the !:RP- -cakulus yieldini lhe

followina result:

Ihtq'ea 5, Let ~ be 1 clause set contain.ing tbe fullCtional rertexivity llioms. Tben:

• ~ J---ERP- FALSB .... ~ is unsatisfiable.

Bnmote. The func:tioQaJ reflelivity uioms are ßHded for the completenets ot tbe I:RP-calculue: Let S ,. {T ,A,B,c.D,Jl)-

• Let a,b,c,d be constants ot sort A.B.c.n reepectively _
• Let P be 1 unary predicate WiUl SO(P) · (B).
• Let r E P with 1 tianature, sucb that [f(t 1 ,t 2 >J · B. iCf <h1J s A and h2l s C) or ( ht1 s Band h2J s D ); otherwise U'<t 1 ,t 2 ß = S.
• Let es be the dau~~e aet { (·b}, {Oid}, (P(f(a,c))}, f,P(f(b,d))J }.

I .bis daute set il UDI&ütfilltle, b ut J: -par1moduJ1lioo is not possible, si1lce [f(b,c)] · [f(a,d)] · S. There is no deductica c:l tbe empty dause in ERP-. Ir tbe func::t..i<lUI refltJivity uioms are prnent, \bell f(a,c).f(b,d) cu be deduc:ed from the .hmc:üonal refleJivity uioms l1ld the clautes in es. Rnc:e the empty clause is tben deducable. 0

Th.is result is somewh1t theoretic:al. In priCtical applications, tbe fwac:t...iclMI refleJivity Uioms are not used. since (i) tbey increase tbe search space enaraously and (ü) tbe subsumption ru.le would delete alt c:l tbem but the uiom 1111. Clearly, th.is omission may be the reuoo ror incompletenets.

1. Iht S<I1-Tblqea. Fot 1 poiymorpbic: sipature s IG and a related diUte set es. we define an un3otted relativir.aUon esrel [WI83, Ob62] as foUows:

For every sort S u11 a unary predicate P 5 .

Thesetot IQft 11io111 AE COIIiiU oC:

• '11 ,ps(I) v pt{l) , jf SsT ror S,T t S.
• '11 Ps(J) for the ..... telt 10tt S ot S.
• '11 t·-···1n ,ps1<1 1 )Y --· vo.Ps.<1n> Y-1Ps..a<r<1 t···-.ln)) ror every r e P and every (S 1 ·... .S 0 ) E SO(f).

The relativi!atioo <Tel ot 1 dause C is the claUte itself, wbere the totts ot the vltiables are ipored and for every variable 1 d C 1 llteral ~JI) is added lO tbe c11use.1Ve have CSret · Ar. v

{C,.etf CE es}_

The followinl tblotea, whäch is proved in [Sch8~al. and w.bich is proved for otber tigaaturn in [Ob62] and [1Va831. states tbe equivaJeftc:e ot tbe sorted and tbe unsorted version ot a cJau· Iet:

Tblgrea 6. (SortenHU) Let Q be a SIG-eoned dause 18\. Tben:

es iJ unsatilf'iable iCf CSret is uuatill'ilble. 0

heppJt, T.bil enmpll il taka froa [SM7Sl, vhidl appean 10 be 1 toldmine ror tbeorea PfOVina enmplta. Durine 1 coune OG autoaated tblotem proving in tbe lut .......... OUf ltUdnU bad &o traatlate tbHe puulel ia&o firlt order precticate lQiic and 10 solve tJaea vith our tblorea prover (Markgraf tarl Refutation Procedure) [lM84l. ODe ot thete probleaa (Problem 47) read1 ·· follaws:

"When AJicle entel'ed 1M foteil ot fwtetfuJMts, sbe did not roraet everyUUDe, onty Cll'tain tJlinat. SM rlten foraot her uae. and tbe 1a01t UteJy to roraet wu tbe day ot tbe vee.t. Now, tbe üaG and tbe unioorn vere fte4Utnt vilitors 10 thil rorelt. T.be· two are sttanae creatures. Tbe liOG lies OG Maadaya, Tuesdays and W'edMtdays aad teilt tbl truUl on the ot.ber days ot tbe weet. Tbe U1lioonl. on tbe otber band üet on Thurtdays, Friclays and S&turday1, but teUI the truth oo UM otber days ot tbe weet. ODe day Alice aet tbe üaG ud tbe uniconl rettina undlr 1 tree. Tbly made tbl foüawina ltltemenu:

l..ioll: Yeswday va one ot my Jyina d1ys. Unicom: Yeawday vu one ~ ay lyiftl daya. Proa tbHe JWeMntl. A1ict vbo was 1 briaht airl. was ablt lO deduc:e tbe day ot tbe vee.t. Wbat was it?"

We use tbe predicates MO(J), TU(x), - , SO(J) ror sayina that I is a Mond1y, Iuesday etc. Furthermore we need the binary predic:ate MBMB, incücatina set Members.bip and 1 3-ary predicate LA. LA(l y z) is true if I saysat day y that he lies at day z; LDAYS(J) denotes tbe ·t d iyial days ot 1. T.be remainiaa symbols .-e self eJplaisWla. One-dulracter symbols li.te u,x,y ,z are reaarded as universa.Uy quantified variables.

Axiomillüon d 1M daya d lbe v·t: MO( I) .. ..('J'U(I)wftx)wTH(J)YJII(J)vSA(J)vSU(l) ) TU(I) .. -(YB(J)wiH(J)wfR(x)vSA(x)vSU(I)YMO(x) ) WB( I) .. -(TH(I)YPR(J)vSA(l)YSU(l )wMO(I)YTU(l) ) TB( I) .. -(PR(J)vSA(x)vSU(J)wMO(J)wTU(l)wWB(J) ) Pl(l) .. 1(SA(x)YSU(I)wMO(J)YTU(I)w1fB(I)YIH(J) ) SA(I) .. -6U(x)wMO(I)YTU(I)YWJ(I)YIH(I)wPR(I) ) SU(I) .. 1(MO(J)wTU(x)Y1VB(J)w'J'H(J)YPI(x)YSA(J) )

AJioaiz&Uoo ot tbe function ynterday:

MO(yestetday(J))

.. TU(I)

IU(ynterday(x))

.. WB(x)

AJiotlilaUaa d tbe fUDCtiaD LDAYS:

MDII(J LDATS(lioll)) · MCXJ)vTU(z)vWB(x)

MIMBb LDAYS(..._a,). TB(JM'I(x)vSA(I)

Axioaür.aüoa d tbe prectic:aW LA:

.,MEMB(J LDAYS(u)) ALA(u J y) · MBMB(y LDAYS(u))

-.MBMI(J LDAYS(u)) A ,LA(u J y) ·

.. MDO(y LDAYS(u))

MIM8(1 LDAYS(u)) ALA(u J y) .... MEMB(y LDAYS(u))

MIMB(x LDAYS(u)) Ml.A(u 1 y) · MBMI(y LDAYS(u))

Tbecna:

h LAUion 1 yelt.erday(J)) A

LA(UDiconl 1 ,...,day(J))

Tbe MOP prod proctdute a1 lllMrtliUWD touad a prod ror lbit U1lJOrWd vertioa lhtt 113 ntaluUoo ttept, amoaa &bla 11 uuece~ ~~ep~, beDI:e lbe fiDal prod ... I 02 ...,. .... Tbil prod COGIIiDI I Iot d trivial ttept carrelp(l)dlfta 10 coamc. Mtllt reuon1na (lite: r today it Maedly, it il oot Tuetday tle.).

Liter uae tort tttuc:lun and tbe tipature d tht problea 11 blad wu IIDifl-.cl autoallic:aUy by 1 ttlllll11« aodull wtucll ICCtfU an UDtOtted c:laule 1tt u iaput and prodUCis t.be equiv.-t aaay­ -1011ed vtflioll toettber wit.b tbe conetpandina sjpatute [Scb85b].

The sott structure ead tbe sjpllure CODtam 111 tbe relevaat WormaUoa lbout tbe retatiolllblp d uury pndic:atet Uite our dlyt) aad u. cloaam-raoaeiOtt reJatioe d fu8dioas. Tbe tort tttucwre d tht sUbiOtU d DAYS Ja out tJiaple il tNtUiVIIeat &o tbe lltüce d ....., d (Mo, Tu, Ye, Tb, Pr, Sa. Sul vi\bout tbe eapty 1tt, ordered by t.be tUblll order. Hence uaere ... 121 ( ·2 7 -l) IOrtl. 1'tle fUDCtion ·ye....,day" il a polyaorpllic: fuDcdlll witb 127 domliD-tort relatioDt ute yetterdly ((MO, YB)) · {SU, TUl.

Tbe Ulliticatioa aJaarlt.hm exploiu tbit Woraation IDd prodlas cmJy UDiiln, wlüc:b retpec:l the 1011 relaUclu, i.e. {J .. t) il l)'!ltal:lic:llty CXJI'reCit. I aad ODiy I Uw 1011 rß t11e term t illns or ....a \be 1011 d tbt v·iable 1. Y·atv· aa example ror utüf'icatioll:

tbe uaitier d xSO.TU and yetWday(y:MQ.TU) is {J .- ynterday(y l: MO) ; y t- y 1:1110 }. Tbe MlRP

tMotell-JifOVina ty$1l 0011~ bat proved .... tbecna ill tbe IOt1H ver._ imadi81.tJy Vld!MK tay UUICHIIt)' atept. TM llnttb d U. ptorl il 6. At tbe pro&ocoa lbon, Ule final tUbllitutbl ia&o tbe tbeortiD diUit VII I._ y:TIL 1'lwt tbe ATP ... round lbt aanm. Tburtday, ia 1 Vflty ..,._, rarward ud huaaaute vay. Bere it a procl paotiOOt

Cl A.U x:Mo MBMI (J LDAYS(lioa))

C2 A.U x:Tu 10MB (J LDAYS(ücm))

C3 A.U x:We 10MB (J LDAYS(ücm))

C-4 AU x:Th MEMB (I LDAYS(Ufticorn))

C5 AU J:Pr MDIB (J LDAYS(uniconl))

C6 Al11:Sa MBMB (J LDAYS(Wlicorn))

Cl AU 1,y:Days u:Aaiaal

MDIB(1 LDAYS(u)) ,LA(u I y)

MDIB (y LDAYS(u))

es A.U x,y:Dayt u:Aaiaal

MIMB(J LDAYS(u)) LA(u J y)

,MJMB(y LDAYS{u))

C9 All J,y:Dayt u:Aaimal

,MBMI(J LDAYS(u)) ..tA(u 1 y)

,MIMB(y LDAYS(u))

Cl o A.U 1,y:Diyt u:Aniaal

-.MIM8(1 LDAYS(u)) LA(u I y) MIMB(y LDAYS(u))

Cll A.U x:Tb+Pr+Sa+Su ,MBMB(J LDAYS(üon))

C12 A.U x:Tu+We+Su+Mo-.YDIB(J LDAYS(utliconl))

Tb A.U 1:1My1

...U(IioG I yetWday(l))

,LA(unicorft 1 yesterdly(l))

C<t,l · C10,1 -. Rl :

AU I:Th y:Days LA(Uni<:onll y) MDIB(y LDAYS(unic:orn))

11,2 & C12,1 ... R2:

A.U J:Th y:Tu+W't+Su+Mo LA(UniCICI'Ill y)

C3.1 · C8,3 ... R3:

A.U J:DIIyl y:W'e MIMB(1 LDAYS(.lion)) LA(Iiotl 1 y)

RJ,l & Cll,l ... l<t:

A.U J:Tb+Pr+Sa+Su y:We LAUion 1 y)

R<t,l. Tb,l -. 15:

A.U J:Th -.LA(uolcotn 1 yesterday(t))

R5,1 & R2,1 ... R6: D

7. CqK;tusiQo. lA a leiUie 1 polyiiOfphic calcu1us ia more eJpretaive 1hlll 1 moeoaotpbic calculua: one fuactioo I)'Jilbol es11nUally de~s IlVetal opetltioGI. All alteraalive formulatioG with 1ddilioaal equalitils and ditlereDl IYIDboll sunly producttlllraer llatcb space.

Tbe ERP--Wculua allows to eJpnu Uaia ialoraatiOil and aives tbe poatjbWty to '* UU. illlor...­ dnctly in Ulle ialerence mecblaila. Thus "' ERP'-calculus Iw 111 Ulle actv.._. d a many IOI'ted Clkulua, but aa ilaHied eJprellive power.

Poayaorptuc udicalioe il iapleanted iA IM MUP tMotea provial sytaea 11 ~ [lM81] and sbows reaartlble iaprove..- iA parUcu&ar in coabiaatJoG vi&ll 1 sott aeaer·WII ataoriUla [Sdl85bl 'Wtlidl IU&oal1ically &rllltloras a aiven probleiD into it' · po(yaorpbäc, aaay-IOtled vettic:a

Tbe Eap--calculUI could advi81FIUUI&y be uted u tbe buil ol a PILI.OG iapAtaeD&aüall, vbete tbe pre11nt (Robinaoa) un.iric:aüoa aJeori&bm vould be repllotd by an aJgoritbm u pr~d in tbil p1per.

ActOQWJtdulMAt.l.

1 wou1d üke to dwlt: my c:oUeaaues H.J. Oblbac:h, A. Herold lAd H.j. Burc:tert lor &Mk' suppen ud lor tbeir belplul ..... lions dutial the lftPit'ltioll ol thia p1per; Cb. Waltbet, vt.o reld a drart ol lbia paper.; Prd. ~- J. SälkaiDD. vho tDCOUrl8ed .. to write thil paper and read au drattl ol tbil paper.

• (])83 CuDDinaham, l.j., Dick, A.j.J., Revrite Systems on a Lattice ol Types. lep. No. OOC 83n,Iaperia1 f.oUete, LondoG SY7 (1913)
• Co83 Cobn. A.G. laproviat tbt llpreuiveAeu ol Many­ IOI'Ied Laak AAAI-83, Wubiaatoe (1983)
• GNU Goiuea. j.A., Metltluet, J. Bquaüty, Types, ModUles and Gentricalor Loaic Pralt ...... jounW ol Loaic Proer1a11Wla. (191-f)
• GM85 Goeuen. JA., ...... uer, J. ~det SaNd .\Jaebtll. Plrtial and Overloldtd Operators, Brrrors ud Inberitance. SRI Repott ( 1985)
• Bay71 Hayes, P. A Loaic d AcUoftl. MICbine lntelliaence 6, Metaaathematics Unit, University d Edinbuqb ( 1971 )

Hea72 Hensc:bl& L.J. N-Sotted Lotic Iot Autom ... d Tbecnta Provma in lfiaber-<lrder Loeic. Proc. AOI Caareteace, Iotton (1972)

8010 Huet, G., Oppen, D.C., Bquaüoaland lewrite lulea, SRI Tecbolal Repon CSL-111, ( 1980)

OlM [lt1 Mark G hpb, Tbe Marqnr lltl le!utaüon Procedure, Memo-SIIII-1111-8-t-01, (1984)

M.t84 Miabra, P.

Towarda 1 T.beary cl typet in PROLOG.lDt.

symp. oe Loek Prograaama ( 1914)

MOU Mya"'cit., A., O'leefe, R. A Polymorpbic Type Sy ... m for PROLOG. Att.ilic:ial Inte11ipßct 23 ( 1984)

(1)62 OberiCbelp, A. Uo~enucbuaau zur aebtiOftiaen Qua1.0I'eDlolik. MatbeaatilcbeADoalen 1 45 (1962)

• Ro65 Robinaoo, J.A. A Macbine-<lritated Loaic Buecl Oll tbe ReiOluUoo Priaciple. JACM 12 (1965)
• Scb85a Sdlllliclt-Scbauss, M. A Maoy-Sott.ed Calculut witb Polymorp.bic PUDdioDJ Bued OG ReiOlutioG and Pltaaoclu1aüoG. Interner Bericbt. Institut lar Informatik, llltertlautem (lotmcomifta)
• Scbl5b Scbmidt-Scbauss, M. Medlanic:al OlMratioD ol Sotts in aau~e S.U. lot.erner Btric:bt. Institut IUt Informatik, lailerllauwrA (lortbc:oaifta)
• Sa78 Smullylll. R.M. Wbat il tbe Naae rl tb.il Book? Prentict 11111 (1978)

Wa83 Wll\ber,C.

A Maoy-Sor1ed cak:ulus Bued Oll Ret01uüon and PlrlaodulatioG.Proc. rl tbe sth IJCAI, l·llrube, (1913)

• w au Wallber. c. UDifk:alioD in Many-Sor\ed Tbeoriet. Proc. d tbe 6th II:AI, PISA, (1984)
• WR73 Woe. L. RobiDJOD. G. Mllillal Modelt aod Retutalioo Coapletnea: Seai~ Proctduret in Automatie Tblona Provbll. lo "Wordproblema .. (W.W.Iooae. P.l. CUDQDtlo, R.C. L)'Jldoll. eds.), Nortb-HoUud ( 1973)