Lukasiewicz logic based Prolog

Math w are&SoftC om puting 1( 19 94)5-29 A Lukasi ewic zLogicBasedP rolog FrankKla w o nn&Rudol fKruse De partm en tofCo m pute rS ci ence Univ e rs it yofBraunsc hw eig Braunsc h w e ig,Germ an y A bstract Prologisapr ogra mming la ng ua gebasedo narestricteds ubseto f cla ssicalr sto rderpredicatel og ic.Ino rdertoo v ercomes omeproblemsofclassica llogictohand leim perfecth uma nkno wledge ,w eprovideaforma lframew orkfora Luk as iewiczlog icbas edPrologsyst em . Theuse of Luk asiew iczlo gicwithit sconnectiont oUlamg amesenablesustodeal wit hpartialinconsist encie sb yin terpretingthet ruth v a luesasrel at iv edist ancetocon t radict io n. W ealsopresen tt hes oft w a retoo lLULOGw hic hisbasedo nthe theoreticalr esultso fthispa pera ndcanbeseena saPrologs ystem forma n y{v al uedl ogic.Applicat ionsofLULO Gt oa nUlamgameand anexa mpleo freasonin gw ithimperf ectkno w ledgearea ls odiscussed. 1In trod uction Clas si cal log i c pro vide s a fram ewo rk for the fo rm ul ati on and im plem en tation o f kno wledge b ased systems. The prog ram ming lang uage Prolog [6, 7] is ba sed on a s ubset of rst o rde r pre dicate l o gic and th us a c o nside ra blen umbe r of a rti ci al i ntelli gence a ppl icati ons is i mplem ented in Pro l og. N ei ther Pro l o g nor class i cal l o gic a re in tended to cop e wi th incom pl ete, con tradictory , uncertain, o r v ague kno wle d ge. B ut these phenomena are often enc oun te red when k no wl edge ba sed system sha veto bede si gn e d. Various theories for the treatment of o ne of these phenomenaofimp erfectknowledge h ave alreadybeendevelop ed. Defa ult log ic [4] deals with 5 6 F.Kla w onn&R.K ruse in co m pletei nform ation.U nc ertain t ycanbehandl edb yp ro babil istic[ 2]or possibi listic lo gic[ 10],whe reasfuzzylogic [12, 17]i sconne ctedtov ag ueness. A llthes ea ppro ac hestoappr ox im ater ea soningarebase donlogical ca lculi , thatwil lal sopro videthe ba sisf orthetr eatm en tofpartially i nconsi sten t kno wle dgef or whic ht heapproac hpresen ted in this pape rissui tabl e.N ume rica la pproac hestoappro xim at er easoning[11,18]arenot cons ideredhere . A no v erv iewonl ogic al ap proac hestoappro xi m atereason i ngcanbef oundin [ 8,29]. The idea t oexte ndPrologtobeabl et oc arryoutappro x im atereaso ni ngis proposedb ym an yauthors[ 3,13,19,21,22,31].Mosto ft he seapproac he sare dev el opedonaheuri sti cbasi sfromanoperationalpoin tofv iew.Theuseof cut{ov alues as in [19]orthem ix tureofdi eren tc once ptsli k eforinstance i n[ 3]reje ctstherigo rous foundationsandconceptso fl ogicprogram m i ng [ 20].Se man tic alaspect sandi n terpretati onsforthet ruthv al ues in theunit i n terv alaren ot considere d.Thege ne ral iz at i onofther esol utionprincipleto thenon{truth{func tionalpossibi li sti clogi c[ 9] canbesee nasanex cepti on i nthi sl ine. Inopp ositi ontohe uristicapproac he s,w eem phasiz etodev el opP rologextensi onst om an y{v aluedlogi csonthebasisofari go rousl ogic alfram e w ork . F ort w o{v aluedlogicitissu  cie n ttoconsi derthesetoft rueorpro v abl e prop ositions.Inm an y {v aluedl og ic itisnece ssarytok eeptrac ko fthetruth v aluesassignedtothepropositi ons.Generall y ,insteadofthee xact truth v alueassoc iatedw ithaf orm ulaonlyl o w erb oundsf orthi struthv alueare considere d.Gene ral iz ati onso fc la ssicallogi cto[0 ; 1]{va lued orfuzzylogi c usingthis ide acanbefoundi n[ 24,25, 26 ]. Althoughsoundnessandc om - ple tenessres ul ts areobtai nedf ortheselo gica ls ystem s,thepri cefort hisi st he additionofnewaxioms andi nfere ncerul esin v olv ingc onstan tsforthetruth v aluesf romtheunitinterva l. Th is le adstothe,f rom ap ractical viewpoi n t undesire d, ee ct tha t there i snoe ci en tpro of pro ce du re .Eac h pro of h as to be v aluated a c cording to the sp ec ied truth v alue sand therefore the `b est' pro of hastobefound,whi chdoes i n general not ex ist. Th us com pl etene ss can on l ybeobtai ned b yaninniten um be r o f pro of steps whic h can of c o urse only b e carrie d out theoreti call y . In fact, w e will sho w that it isim p os sibl e to o btain com ple teness fo r a [0 ; 1]{v al ued log i c withou t the notion o f i n ni te pro ofs und e rv ery general ass um ptions . Note that com ple teness is here no t understo o d a s o nlybeing a ble to infer all tauto lo gies, since the prop ositio nal calculus of [0 ; 1]{valued Luka siewicz lo gic iscomplete in this sense [5, 27].We A Luk asie wi czL og ic Ba se dP rolog 7 requi realsotobeabl etoderi ve proposi tionsfromagi ve ns et of addi tional ax iom s(akno wled ge base)andtocom putethec orresp ondingtruthv al ues forthed eriv ed pr oposi tions. Inordertopro vi dea logicalsystemsuitableforc om pu te ri m pl em e n tati on, w econsi de ro nlyni tel ym an ytruthvalues,w hic hdoesnoti m posese ve re restric tionsforpractical appli cat ions.Inan ycase, no ex pe rtw ork ingwith arulebase dsystem canbeexpecte dtohandl eal arge ore v e naninni te n umb er of truthv al uesreasonably .B eside sthi stec hnicalrestrictionw eal so stresstogi v eani n terpret at io nforthetruthv al ue s.Th is proble misoften ignore di nothe ra pproac he s.I nordertoha v esu ch ani n terpre tati onw ec hose n {v alue d Luk asi ewiczlogi cforwhi c ham eaningforthetruthv alue sca nbe establ ishedonthebasi sofU lam games[ 23].Onthisbasi s,w ea re ab l eto handl ep ar ti al lyc on tradic toryi nfo rm at ion. Thep aperisorganiz edasfoll o ws. Secti on2pro vide stheform al fram ew orkfora Luk asiewiczl ogicbasedPrologsystem fromapurel ym athem ati cal vi ewpoin twi thoutgiv ingac onc retem eaningtothetruthv al ues.W eobtain soundnessandcom ple tenessre sul ts.Sec tion3isde v otedtothe i n terpre tationofthet ruthv aluesasre lativ edistancetocon tradi cti onm oti v at edb ythe connecti onbet w eenUlamgam e sand Luk asie wicz logic[23] .Thetheoreti cal resultsofsec tion2arei m plem en te dinasoft w aretool call edLULOG,whic h isdescrib ed insecti on4.Exam ple softhea ppli cationofthesoft w are to olto anUl amgam eanda typi calex am pleforrulebaseds yste m swithi m perfe ct kno wle dgearediscussed in se cti on5. 2AL anguagefor A pp ro xim ateRe as oning Basedo n n {V alue d L uk asie wicz Lo gic This sec tion is d e v oted to the form al an d tec hnical ba c kgrou nd o f the l ogi ca l system dev elop e di n this pap e rf rom a p ure ly m athem ati cal poi ntofvie w. A p ossible i nterpre ta ti o n for the set of truthv alues w i ll b e discussed in the follo wi ng secti on. Toa voi d the i ntro duc tion o f a ddi tiona l a x iom sand infere nce r ul es, w e sepa rate the logicall a ngua ge from the tru t hv alues a nd do there fo re not integra te the tru th values as sp ecial logical symbols into the language as it is pro p o sedin[24, 25, 26]. 8 F.Kla w onn&R.K ruse We as sum e L tobearstorder lo gica ll anguagecon taini ng thel og i cal connect iv es ! ,as et L = f8 1 ;:::; 8 k g ofbinaryc onnec tives,theunary connect iv e : (negation) ,andtheuniv ersa lq uan ti er 8 .W ellf ormedf or mulae are denedintheusualw ay . F orthi slogical lang uagew ec onside ranites et T oftruthv alues.Si nce we will mainl yconc en trateon( n +1 ){ val ue d Luk asie wiczl og ic ,w ed ene withoutlossofgenera lity T = f 0 ; 1 n ;:::; n 0 1 n ; 1 g : Witheac hl ogica lconnecti v ew eassoci ateatruthfunc tion. ! i sassum edto bethe Lu kasi ewic zim plic ati on,i.e. we associatethetruthfunction v al ! : T2T!T ; ( s ;t ) 7! m in f 1 0 s + t; 1 g with ! .F ortheconne ctiv esi n L w er equi rethecorrespondingtruth functi onstoben on{decre asingi nbothargumen ts.T ypicall y ,theseconnectiv es wil lbein te rpretedas A ND or OR operators.Throughoutthispaperw ewil l m ain l yconcen trateonthefol lo wingt w ogene ral iz ati onsofthe l ogic al A ND . v al ^ : T2T!T ; ( s; t ) 7! m in f s;t g and v al 3 : T2 T! T ; ( s;t ) 7! m ax f s + t 0 1 ; 0 g : Thenoti on of a T {v aluedi n terpre tati on of L i sde ne dasincl assica ll og i c (com parefori ns ta nce[ 20] ,p.12),exce ptt hatt he se toftruthv alue si s T i nste adof f 0 ; 1 g .Thet ruth v al ueassi gne db ya T {v aluedi n te rpretation I to aform ul ae ' i sdenote db y ='= I ,or shortly ='= wheni ti so bv ious to whi c h interpretati on w e ref er. F or the univ ersa l qua n tier w ede ne = ( 8 x )( ' ( x )) = = inf x f =' ( x ) = g . Be fo re w e can dene the notion o f a m ode l,w eha vetoge ne ra l iz e the conce p t o f a set of axi om s . Instead of a c risp set o f a xi oms whic hisuse din cl as sic a l logic to c hara c teri ze a theory ,w ec o nside ra` T {fuzz y set' o f a x iom s, i.e. a m apping a : L !T .Incl assic al logi c, where T = f 0 ; 1 g , a co rre sponds to the c ha racte ristic function of the set of axiom s. Note that if w e use this cha racteristic function in class ical log icinstea d o f the co rresp onding set of axioms, the a ssignmentofthevalue0toaformula ' by a d o es not mean A Luk asie wi czL og ic Ba se dP rolog 9 that ' isf al sei nthetheory givenb y a ,si nceitm i gh tbepo ssible toderiv e ' fromtheaxioms.T herefore,thev al ue a ( ' )should be unde rstoodasalo w er boundfort he truthv alueof ' .Thi sleads to thefol lo wingde ni tion of a m od e l. Denit ion2. 1 L et a : L !T .A T {va lu e dinter pr etation I of L isc al le d am o delof a if ='= I  a ( ' ) ho ldsfora ll ' 2 L . Th ( a ) : L !T denotest he in mumo verall T {value din terpr etati onsof L thata r emo d elsof a . We saythat a implies ' 2 L toatr ut hd e gr e eofatle ast  ,d enoted by a j =  '; if Th ( a ) ( ' )   holds. No wthatwe ha v edenedthesem an ti calpa rt ofourlogicalsystemw e canturntothesy ntac tic alpartb ypro vi dingaproofproce dure.B utbefore w edothi s,w eel ucidatewh yitisim possi bletodeneaso undniteproof m e thodwhich le adstoc om plete nesswithre spec ttothenoti onofam odel gi v eni nde niti on 2. 1i fw eal lo w T =[ 0 ; 1] . Exam pl e2.2 Letusf or them om en tassum e T =[0 ; 1]. We consi derthe proposi tionall angua ge L whic hc on tai nsonl yonepropos itionalv ariable ' 1 . Thelogicalc on nec tiv esin L are ! ; 3 ; and : where = : '= =1 0 ='= .Letus abbre viate ' 3 ::: 3 ' |{z} m time s ' b y ' m .Let A = f ( : ' 1 ) ! ( ' 1 ) m j m 2 IN and m  2 g and le t a : L ! [0 ; 1] ; ' 7! ( 1if ' 2 A 0ot he rw i se. It is easy to verify that thisimplies Th ( a ) ( ' 1 )= 1. For a ny nite subset of B  A there exists a n m 0 2 IN such that fo r all m>m 0 wehave 10 F.Kla w onn&R. Krus e ( : ' 1 ) ! ( ' 1 ) m 62 B .I tise asytoc he c kthat thei nterpre tati oninducedb y =' 1 = = m 0 m 0 +1 i sam odelof b : L ! [0 ; 1] ;' 7! ( 1if ' 2 B 0otherwi se . Th usTh ( b ) ( ' 1 )  m 0 m 0 +1 holds.A n yp ro of procedurewhic hi sall ow ed to carryoutani ten um berofste ps to de riv ethetruthv aluefor ' from a or A ,re spec tiv ely, canonl ym ak euseofanites ubse t B ofform ulaein A (ex cept if therei ssom e thingl ik eani nniteinfere ncerul e).B uti ft hi sproof proc edurew oul dy ie ldthev al ue1for ' 1 ,i tw ou l dassi gnthi sv aluealready to ' 1 ev eni f B i sassum edtob et he setofaxi om s.Thisw ould im plythat the proofproce durei snotso und. Le tusno wcon ti n uewi thadeniti onofaproofproce durefor ou rlog- i calsystemwi thaniteset T oftruthv al ues.Si ncew eareheadi ngfo r agenerali zationofaPrologli k el anguagean dinordertoobtai nasim pl e proofproc edurew ewil lr estrictoursel v e sfromnow ontoHornclausel ik e ex pressi ons.Whatthi sm e an sisstatedi nthefoll o wingtw odeni tions. De ni tion2.3 A nimplic a tio nc lauseisaclose dwellfo rme df ormulaofth e for m ( 8 x 1 ) ::: ( 8 x k )( ' ! )( 1) or ( 8 x 1 ) ::: ( 8 x k )( ) ; ( 2) wher e isan atomicformula withnootherf r e evaria blest han x 1 ;:::;x k . ' isa fo rmula c ontainin g only c onne ct ives b el o n gin g t o L a nd no qua n tie r s. Im plic ati on cl au ses do not al lo we xiste ntial quan tiers, whi chisofc o urse ar estri ction. W e do not cons i dere xisten tial q ua n tiers here,i norde rtoobtain a logical system sthatc an b e u sed for i mple men ta ti o n an d cant herefore not av oid so m eres tric tions. In princi pa l ,the proble mof rul ing o ut e xisten tial quan tiers c oul dbeo vercom eb ysk olem ization. As `fuzzy' Pro lo g prog ramsweaccept only `fuzzy'setsofaxioms a : L ! T that restrict to implication cla uses. A Luk asie wi czL og ic Ba se dP rolog 11 Denit ion2. 4 Amapping a : L !T is calle da T { L {Pr olo gpro gr am if onlyim plic ation cl ausesb elongtothesupport of a ,i .e. a ( ' ) > 0 impliesthat ' isanim pl ic ationclause. Thecl assic aldeducti on sc hem atam oduspone nsands ubst itutioncan bee asi lyi nc or poratedin toourl ogic al sy st em .Ofc ourse,w eha v etok eep track ofthec orre spondi nglow er bo undsforthetruthv al ues . Inp art(i ) ofthefoll o wingde n itionthecal cul ati onofgreatestlo w e rboundforthe correspo ndingtruthv al uesbasedon thet ruthf unc tion ! isincorp orated in to thededucti onsc he m atam od us ponensandsubsti tution. Denit ion2. 5 L et a ;b : L !T b ea T { L {Pr olo gpr o gr am. (i) b isd ir ec tlyd er ivablefr om a if (a) th er eexistsanimplic ationc lause ( 8 x 1 ) :: : ( 8 x k )( ' ! ) i n L such tha t ( a1)I f 0 isanimplic ationclausewithfr e evariables x 1 ;:::;x r and 0 6 = ,then a (( 8 x 1 ) ::: ( 8 x r )( 0 ))= b (( 8 x 1 ) ::: ( 8 x r )( 0 )) . ( a2) b (( 8 x 1 ) :: : ( 8 x k )( ))=m ax f = ( 8 x 1 ) ::: ( 8 x k )( ' ) = a + a (( 8 x 1 ) ::: ( 8 x k )( ' ! )) 0 1 ; a (( 8 x 1 ) ::: ( 8 x k )( )) g ; (3) wher ethevalue = ( 8 x 1 ) ::: ( 8 x k )( ' ) = a isobtaine dbyc onsideringth eHerbrand univers eof L andvaluating atomicfor mulae ac c or dingt o a , hol ds or (b) t her e e xists an implic ation c lause ( 8 x 1 ) :: : ( 8 x k )(  ) and te r ms t i 1 ;:::;t i r ( i 1 ;:::i r 2f 1 ;:::;k g ) w ithout fr eevar iab les su ch that for t he f ormula  0 , which is ob taine d by sub stitutin g x i j ( j = 1 ;:::;r ) by t i j in  an d qu a n tifying over t he r e maining fr eev ariab le s, b (  0 )=max f a (( 8 x 1 ) ::: ( 8 x k )(  )) ;a (  0 ) g : (4) is satised. 12 F.Kla w onn&R. Krus e (ii) b isder iva blefr om a ,a bb re viate dby a<b ,if ther eisase quenc e a 0 ;:::;a n : L !T of T { L {Pr olog pr o gr amswher e a k +1 isdir e ctly derivable fr om a k fore ach k 2f 0 ;:::;n 0 1 g and b  a n holds. (iii)Themapping th ( a ) : L !T isgiven by th ( a ) ( ' )= 8 > < > : sup f b ( ' ) j a<b g if ' isanimplic ation cl ause ofth eform (2) 0 oth er wise. (iv)A nimplic atio nclause ' 2 L ofthefor moftheform (2) isder ivable fr om a withatruthdegr e eofatle ast  2T ,abbr eviate dby a `  '; if th ( a ) ( ' )   h olds. Theappli cationofm odus ponensandthesubstituti ono ffreev ariables by otherte rm sisfor m al iz edin( i )(a)and(i )(b),respe ctivel y ,intheabo v e deni tion.(i i)desc ribestheappli cationofa ni ten um be rofdeducti on stepsoftheformin troducedin(i ).Si ncew eassum e T to betheni te c ha i n f 0 ; 1 =n;:::; ( n 0 1) =n; 1 g thesupr em umin(ii i)i si nfac ta m axi m um . Th us,f or allim pl ic ati onc lause s ' oft hef orm(2),theree xistsa T { L{Prol og program b ' deri v able from a suc hthat b ' ( ' )=th ( a ) ( ' ). Ex am ple2.6 Conside rthefo llowingthre el ogic alform ulae anda T { L{ Prologp ro gram a ,where T = f 0 ; 0 : 1 ;: ::; 0 : 9 ; 1 g ,thatassignsthei ndicated v aluesto thesef orm ulae. ( 8 x )( P ( x ) ^ Q ( x ) ! R ( x ))0 : 9 P ( X 0 ) 0 : 8 Q ( X 0 ) 0 : 7 where P; Q ,and R are sym bol sforpr edic a tes an d X 0 is an indiv idua l con - sta n t. T o all other form ul ae ' the v al ue zero i sassi gne db y a .Appl ying p art (i )(b) of Deniti on 2. 5torstf orm ula, w e can de riv e P ( X 0 ) ^ Q ( X 0 ) ! R ( X 0 ) 0 : 9 : (5) A Luk asie wi czL og ic Ba se dP rolog 13 Techni call yspe ak ing,w ec an de riv efrom a the T { L{Prolog prog ram b that assignsthesam ev al uestoform ul aeas a ,except fort heform ul a P ( X 0 ) ^ Q ( X 0 ) ! R ( X 0 )towhic h b assignsthev alue0.9. Assum ingthat =' ^ = =m ax f =' = + = = 0 1 ; 0 g isthetruthfunction assoc iatedwith thec onjunc tion ^ ,part(i)(a2) of Deni tion2. 5appli ed to equation (5)yi el ds R ( X 0 )0 : 4=m ax f m ax f 0 : 8+0 : 7 0 1 ; 0 g +0 : 9 0 1 ; 0 g whenw et ak ethev alue sassi gne dt o P ( X 0 )and Q ( X 0 )in to accoun t.Th us w eha v esho wnth ( a ) ( R ( X 0 ))  0 : 4.I nfac t,w eha v eev ent h ( a ) ( R ( X 0 ))=0 : 4, sincetheproofi st heonewhi c hgi v e sthegreatestv aluefor R ( X 0 ).W em a y al sowrite a `  R ( X 0 ) foran y  2f 0 ; 0 : 1 ;:::; 0 : 4 g . Theore m2. 7 L et a : L !T b ea T { L {Pr olo gpr o gr amandlet ' b ean implic ationclauseofthefor m (2) .Then th ( a ) ( ' )  Th ( a ) ( ' ) holds. Proof. W eha v etopro ve that,if I isam odelofa T { L{Pro l ogprogram then I isal soam ode lforan y T { L{ Prologprogramdire ctly deriv abl efrom thegiv en T { L{P rologprogram .Let I beam od el of a andle t b bedir ectl y deri v ablefrom a . Cas e1. b i sobtainedfrom a by applyi ng(3). Since I is am od elof a andac cording to them on otoni ci t yofthet ruth functi ons in L ,w ed eri ve = ( 8 x 1 ) ::: ( 8 x k )( ) =  max f = ( 8 x 1 ) :: : ( 8 x k )( ' ) = + = ( 8 x 1 ) :: : ( 8 x k )( ' ! ) = a 0 1, = ( 8 x 1 ) ::: ( 8 x k )( ) = g  max f = ( 8 x 1 ) ::: ( 8 x k )( ' ) = a + = ( 8 x 1 ) :: : ( 8 x k )( ' ! ) = a 0 1, = ( 8 x 1 ) ::: ( 8 x k )( ) = a g = b (( 8 x 1 ) ::: ( 8 x k )( )) : 20 F.Kla w onn&R. Krus e Thea nsw e rtotherstq uery yi elds thetruthv al uewithwh ic ht he pre di cate has{feathers holds for t w eet y ,whe reasthes econdq ue ryl istsallindiv idua ls, towhi ch thet wo predic ate s anim al and ha s{feathe rs apply ,andcomputes for eac hi ndi vi dualthe Luk as iewiczconjunc tionofthec or re spondi ngtruth v alues.Thelast queryyi eldsal lpredi catesw itht hec orre spondingtruth values whic hc anbeappl iedto tw ee ty . M oree xam ple sforen tri es in the kno wle dgebaseandqueri es canbefoundinsect ion5. Thebasici nfere nce me chanismofLULOGi sm oduspone ns .B esides m oduspone ns substi tutionofv ariables is ne cessary .Aproofforaq ue ry is found b ybac kw ardc haini ng,i. e. if w ew an ttopro v e ' ( x;y;:::;z ),w elook forfac tscon tai ning ' ,yieldi ngdi rectl yatruthv alue, orforrul eswi th ' in the head,andthenunifythebodyo ft he rulecorrespondinglyandc on ti n ue withtheu niedp redic ate si nthebodyo ft he rulei nthesam ew a yun til w ereac hafactaga in.Ifaproofi sfoundb ythi sp ro cedure ,thebac kw ard c ha ininghastoberetrace di nthe oppositedi recti oninorde rt oc om putethe correspondi ngtruthv al ue.N otethatw eh a v etondtheproofy iel dingt he m axi m altruthv alue,sot hatw ec anstopthesearc hproc edureonly ,when w eha v efoundaproofthat giv esthem axi m altruthv alue n appeari nginthe setoftruthv alues,orwhe nallp roofsareexam i ned. Ifiti snotnec essarytond thegre ate stderiv abletruth v al ueforaquery , one ma yalsoin terrupttheprogramL ULOGi nordert ogetthev alueo f thebestprooffoundu n tiltheti m eofi n ter rupti on .I norde rtoi ncrease thec hance sforndi ng good proofsinanearlystateo ft he searc h,LU LOG c ho os e stherul etowhi c hthehighesttr uthv al uei sassi gned,w he nthereis m orethan onepossibler ul eforthebackwardc hai ningprocedure . 5ApplicationExam ples In thi sse ction w edi scus s the appli cation o f our Luk asiewi cz l o gic ba sed Prolog syste mto t woe xam ple s. F or those re ader s w ho are fam ili arwi th the prog ramming l anguages Prolog and Li sp, w eha ve also writt en do wn parts of the dial og wi th the m ac hine . Ex am ple 5.1 The  rst ex ampl eisv ery sim pl e a nd do esnotin volv ean y cha ined inference. We try to solveanUlam gamewith S = f 1 ; 2 ; 3 ; 4 ; 5 g as the set from whichthenumberto begues sed ischo sen and a p ermission A Luk asie wi czL og ic Ba se dP rolog 21 QuestionA nsw er Q 1 Then um be rtobeguessed is aprim e.no Q 2 Then um be rt ob eguessedisev en.y es Q 3 Then um be rtobeguessedi se ven. no Q 4 Then um be rto be guessedis1or5.no Q 5 The numb e rtobeguessedisasquar e. yes Q 6 Then um be rtobeguessedis less than4.no T able2:A nUlamgam e. ofam axi m umoft wo lies.There fore,asex plainedi ns ec tion3,w eha v eto c hoosea4{v aluedlogic.A sm en tionedi nsec tion4,we ta ke theset f 0 ; 1 ; 2 ; 3 g as truthv aluesinsteadof f 0 ; 1 = 3 ; 2 = 3 ; 1 g .Thei n te rpre tationo fthesetruth v al uesi s 0:m orethant w oli es 1:t w oli es 2:onel ie 3: no l ies. Ta bl e2 sho wsaprotocolofanUla mg am e.Inorde rtom ak euseofo ur Luk asiewiczlogi cbasedPrologsystem ,w ein tr oducesi xpre dicates an sw er1 , ::: , answ e r6 .Startingfromanem pt ykno wledgeb as e,w eaddfore ac h i 2f 1 ;:::; 6 g ande ac h s 2 S = f 1 ;:::; 5 g thefac t answ er i ( s )wi thtruth v al ue 2( l ie)i fthen umb er s w ou ld make theansw ertoques ti on Q i alie, and with truth v al ue 3 ( no li e) i f the a nsw erto que sti on Q i is correct, ass um ed tha t s is the n um berto beg uessed. A s an exam pl e the corresp onding en tri es in the knowle dge base for Q 1 and Q 5 are s ho wnintabl e3. In o rde r to see, ho wm anyli es a re u nde r the a nsw ers for e ach s 2 f 1 ;:::; 5 g ,w esi mply ha veto c om pute the Luk asiewi cz conjunctio n for e ac h s . This is done a utom atic al ly b y the Luk asie wi cz l o gic bas e d Prolog when we as k for the truth v alue of the Luk asiewi cz conjuncti o n o f the predi cates answer i for a n on{s p ecied variable. The truth value 3,2,1, a nd 0 corresp ond to no lie, one lie,twolies, more than th reelies. Table4 shows the 22 F.Kla w onn&R. Krus e s Q 1 Q 5 1 (AS SER T!(A NSWER1 ON E3))(AS SER T!(A NSWER5 O NE3)) 2 (AS SER T! (A NSWER1TW O2))(AS SER T! (A NSWER5T WO2)) 3 (AS SER T! (A NSW ER1TH RE E2 ))(AS SER T! (A NSW ER5T HRE E2 )) 4 (AS SER T! (A NSW ER1FO UR3) )(AS SER T! (A NSW ER5F OUR3) ) 5 (ASSER T! (A NSW ER1FI VE3) )(ASSER T! (A NSW ER5F IVE2) ) T abl e3:En tri esinthekno wledgebasefor Q 1 and Q 5 . ?X=1 =FIV E?X=0 =F IV E ?X=2 =F OU R?X=2 =F OU R ?X=1 =THR EE?X=0 =T HR EE ?X=1 =TWO?X=0 =T WO ?X=2 =ONE?X=0 =O NE T abl e4:Thestateofk no wledgeafterther st3(l eft)and 6(righ t)answ ers. resul tsaftertherstt hr eeansw ersandafterallsix answ ers,re spec tiv ely . Thecorresp ondingresultsareobtai nedb ytheLULOGcom m ands  ( AND *( ANS WE R1?X) (A NS WER 2? X)(A NSW ER3? X)) and  ( AND *( ANS WE R1?X) (A NS WER?X )(AN SWE R3?X ) (ANSW ER4?X )(AN SWE R5?X) (ANS WE R6?X) ) , respecti v ely . From ta bl e4 w e can see tha t after the rst three a nsw ers stil lal lnumb ers are p os si ble, but afte r six ans w ers w ekno w that the c orre ct guess m ust b e 4 (corresp o ndi ng to one li eonl y). Ex am ple 5.2 In this e xa m ple w e discuss a sho rte ned version o f the te st{ example examined in [29]. The fo llowin g sta tementshaveto be integ rated into the knowledg e base. A Luk asie wi czL og ic Ba se dP rolog 23 (s1) Studen tsarey oung. (s2 )Y oungpeoplearesingl e. (s3) Studen tswhoha v ec hil drenar em ar ri edorc ohabitan ts. (s4)Cohabitan tsarey oung. (s5)Single ,m arrie d,andcohabi tan taremutual lyex clusi v e. Inordertodescri be the sestate m en tsi naform all anguage ,theunary predic ate s sd n t ( x ), yng ( x ), sng ( x ), pn t ( x ), m rd ( x ),and c h bt ( x )areint roduced, meaningthat x isre spec tiv elys tu de n t,y oung,si ngl e,paren t( ha ving oneorm orechil dren),m arrie d,andcohabi ta nt. Inaddit ionw eusethe proposi tion c n tr for re presen ti ngac on tradi ction. Only(s5)i sunderstoodasapropositionincla ssic allogi c,theothe rstatem e n tsaretrueinm ost, butnotinallcases.Thestate men ts,f orinstanc e (s1),c anbewri tteninProl og{ li k est ylei ntheform yng(x) sdn t(x) : Sincew ec annot besurethat(s1)alw a ysholds,w eha v etoassi gnanappropriatetruthv alue to thi srule,indic ati ngther el ati v edistanc efromc on t ra - diction.W ec hoosea7{v al ue dl ogicw iththetruthv alues0 ;:::; 6. Thetruth v al uesa ssignedtothestatem e n ts(s1), (s 2),and(s4)are5,4,and4 ,r espe ctiv el y .(s3)can notb erepresen t eddirec tlyi nt he languageLULOG,sinc e intheheadofarul enoc onjuncti onsordisjuncti ons area dm i tted.I nthis case, w ecanm ak euseofthefa ct that m arri edandcohabi tan ta re mutuall y exc lusiv e, splittin g( s3 )in tothet w orule s (s3a ) Studen ts wh o ha vec hil dren a re m a rri ed. (s3 b) Studen ts wh o ha vec hil dren a re c o habitan ts. We a ssign to eac h rule the truth v al ue3sothat the Lu k asie wi cz conjunction o f ` marrie d' and `c o habitan t' o btained from these rules, when w e are deali n g with a studen t with c hildre n, a l ways yie lds the v al ue0. (s 5) is expres sed by the fo llowing three rules, again written in Prolog {like style, which a re always valid and a re therefore a ssigned the truth value 6. 24 F.Kla w onn&R. Krus e Entryinthekno wle dgebas e (s1) (AS SER T!(R ULE( YNG?X )( SD TN?X)5 )) (s2) (AS SER T! (R ULE( SNG?X )( YN G? X)4) ) (s3a) (AS SER T! (R ULE( MRD?X )( AN D( SDT N?X)( PNT? X ))3)) (s3b) (AS SER T! (R ULE( CHB T? X)(A ND(SD TN? X) (PNT? X))3) ) (s4) (ASSER T! (R ULE( YNG?X )( CH BT?X)4 )) (s5a) (AS SER T!(R ULE( CNT R)(AND*( SNG?X )( MRD?X ))6) ) (s5b) (AS SER T!(R ULE( CNT R)(AND*( SNG?X )( CHB T? X) )6 )) (s5c) (AS SER T!(R ULE( CNT R)(AN D*(M RD?X )( CHB T? X) )6 )) T able5:Thek no wl edgebaseforexam pl e5.2 . ( s5a) cn tr sng ( x ) 3 m rd ( x ) (s5b) cn tr sng ( x ) 3 c h bt ( x ) (s5c ) cn tr m rd ( x ) 3 c h bt ( x ) Theuseofthe Luk asi ewic zc onj unc tionfor(s5a){(s5c )a dm i tsthepossibi li t ythatapersonm i gh tbeaas signednon{zerot ruthv alues fo ral lthe threepredicates sng,m rd ,and c h bt ,but stil lha v ingthetruthv alue0 for cn tr . Thishol dsasl onga st hesumofthetruthv alues of tw oofthe sepre dicates is al wa ysl essthan6.I tm e ansthat we areacce ptingaparti alc on tradic tion. Thecomple te kno wledgebasei nLULOGi ss ho wni ntabl e5. No wletusassu me that w ekno wthatLeai sastudent andthatsheis possibl yam other,s ince we sa wherwi thac hi ldresem blinghe rfaceonthe cam pus. Sow eaddtothek no wledge thet w ofacts sdn t (l ea)a nd pn t (le a) with truth v al ue 6 a nd 5 , resp e ctiv el y.A sking th e question wh o is single,w e obta i n the an sw er that sng (lea) is satised w i th truth val ue 3 (a nd no m ore indi vi duals are li ste d, sinc e sng cannotbeappl ied to s om eone el se inc luded in the kno wle dg e base at the m om en t). A sking fo r cohabi ta n ts or m arri ed p ersons w e get that chbt (le a) or mrd (l ea)bothhol d with truth v alue 2. Althou gh single, co habitan t, and m arri ed are m utuall yexc lusiv e, w e o btain that cn tr (c on tra di ction) ho l ds w i th truth v al ue 0 . This is due to the l ow truth value fo r chbt and mrd ,so thatwe still can accept this pa rtia l contradiction. Tab le6shows a LULOG proto col of the corresp o nding questions and answers. A Luk asie wi czL og ic Ba se dP rolog 25 Addi tionale n tri esf orthek no wle dgebase (A SSE RT !(SDN TL EA 6) ) (A SSE RT! (PNT LE A5)) Questi onAnsw er (S NG?X )? X=3=LE A (M RD?X )? X=2=LE A (CHBT ?X)? X= 2= LE A (CNTR )V al id wit hval ue0 Table6:TheLULOGdi alogueconcerningLea. Addi tionale n tri esf orthekno wle dg ebase (A SSE RT! ( SDN TP AU L6 )) (A SSE RT !( CHB TP AU L6 )) (A SSE RT !( CHB TL EA6) ) Questi onA nsw e r (S NG?X )?X= 3=LEA ?X= 3=PAU L (C NTR )Va li dw ithv alue 3 T able7:TheLULOGdi al og ue conce rningLeaandP aul. Letusnal ly a ssum e that w ele arn that P aul who i sal so a studen tis Le a' scoh abitan t. So w eadd the f act s sdtn (pa ul ), chbt (pau l ), and ch bt (lea) with truth v al ue6tothek no wl edge base. When w eno w ask for si ng l e pe opl ew e obta i nthatthepre dicate sng holds with truthv alue 3 for Lea as w ell as for P aul . Tog ethe rwi th the kno wle dg e th at Lea and P aul are coha bita nts , this leads to a value of 3 for cntr (contra diction). The protocol o f the corresponding LULOG dialogue is s hown in ta ble7. 26 F.Kla w onn&R. Krus e 6C onclusions W eha v epro v ided af orm alfram ew orkfora Lu kasiew i czlogi cbasedProl og andh av ed iscussedasoft w areto ol whic hw asdev el opedonthis theoreti cal basi s.Inpri nci palitispossibletodropthere stri ctio nt oanitesetof truthv al ue s,e sp ec iall ysi nceinprac ticew ea lw a ysha v etodealwi thani te kno wledgebase.B utthei n troducti on ofre aln um bersfromtheu ni ti n terv al astruthv aluesw oul denforceustogiv eupt hesim plei nte ge rope rati onsf or theni te{v al ued case.Thisi sasev eredisadvan tagesince ,inoppositi onto ordinaryProlog,w eha v etol ookfortheproofy iel dingthegreatesttruth value.Thism e ansthatw eha ve to se arc hthroughthewholepr ooft re ein allca ses, whic hisofc oursem uc hmore co mpl exthanbre ak ingupaftert he rstproofi sf oundasi tisdonei nProlog. W ehav euse dt he Luk asiewi czim pl ic ati on forsem an ti calre asons,i norder tobeabl etoapplyt hein te rpretationofthetruthv aluesof Luk asie wi czlogi c i n troduce db yMundici[23 ] .Thetheoreti calresultsof se ction2arestil l v ali dforotheri m pli cationoperatorsli k etheG ode lim pl ica ti on.Ofcourse , eq uati on(3)indenit ion2.5hastobem odi e dac cordi ngl y .T oadaptthe m odicationforthesoft waretoolLULOG,onl ythi sformul ause di nthe v aluationofproofshastobere dened. AsordinaryPrologt he LU LOGsystemisonl ybasedo nare stri ctedsubset of rsto rderlogic,m ai nlyb ya void ingnegati on.A ne xtension to th eful l calc ulus of rst order Luk asi ewic zlo gicw ouldl eadtothesam ecomple xi ty andundeci da bi li ty prob l em sthatappeara lr ea dy forc lassi callogi c,s ince cla ssic allogici sincl udedinLULOGsi m pl yb yc hoosing f 0 ; 1 g asthesetof truth v alues. An d in con trast to classical log i c, w e a re in the ba d si tua ti on that rst o r de r Luk as i ewic zlogi cisnotcom pl ete [ 28]. Ne verthele ss, LU LOG ca n cop e with v arious pro bl em sconne cted t ore aso ni ng w i th pa rti ally inc o nsistent kno wle dg e. In m an yothe rfu zz y Pro l og system s often o nl y the pro of pro cedure of Pro l og is fuzzi ed so that i tisim - p o ssibl e to desc rib e suitable sem an ti cs for suc hsystem s. L U LOG i s based on a pure logical a pproa chwhere synta x and semantics a re strictly separa ted, gua ranteeing fo r a clear interpretation o f the system. A Luk asie wi czL og ic Ba se dP rolog 27 Referen ces [ 1]B.M .Ay yub,M. M.Gupta ,L .N .Kanal(e ds. ),A nalysis andM anagem e n t ofU ncertaint y: Th e oryandAppl icati ons.N or th{Holl and,A m sterdam (1 99 2). [ 2]F.B ac ch us,Re presen ti ngandReaso ni ngwithProbabi li sti cKnowle dge. MITPress,Cam bridge,Massac h usetts(1990). [3]J .F.Baldwi n,F astOperations on F uzzySetsi ntheAbstrac t Fri l M ac hi ne.Proc.I EEEI n te rn. Conf.onF uzz ySyste m s,SanDi ego(1992), 803{809. [ 4]P .Besnard, DefaultLogi c.Spri nger{V erla g,Be rli n(1989). [ 5]C. C.Chan g, A lgebraicA nal ysisofMany{V aluedLogic s.T rans.Am e ricanMathem ati calS oc i et y88(1958),467{490. [ 6]W. F.Cl oc ksin,C.S.Mel lis h,Program m i ngi nLogic(2nde d. ).Springer{ V erl ag, B erl in(1984). [ 7]R.Cordes,R.Kruse ,H .Lange nd orfer,H.Rust,Prol og(3rde d.)(in Ge rm an).Vi ew eg,B raunsch w ei g(1992). [ 8]D.Duboi s,J.Lang,H. Prade ,F uz zySetsi nA ppro xim at eRe asoni ng, P ar t2 :Logi calA pproac he s. FuzzyS etsandSystem s40(199 1),2 03 {244. [ 9]D.Dubo is,H .Prade,Resoluti onPrinciple sinP ossi bili sticLogi c. In te rn. Journ.A ppro x im ateR ea soni ng4(1990),1{21. [10]D .D ubois,H.Prade ,E pistem ic En trenc hm en tand Poss ibilisticLogic. Arti c ial In tell igence 50 (1991), 223-239. [11] D . Du b ois, H. Pra de, Fuzzy Se ts in Appro xi mate Re ason i ng , P art 1: Inferenc ewi th P os si bili tyD istributi ons. F uzz y Set sand Sy ste ms40(1991), 143{202. [12] S . G ott wal d, F uzzy Se ts and F uzzy Lo gic .Vi ew eg, Wi esba de n (19 93). [13] M. Ishizuka, N. Ka isa i, Prolog {EL F Inco rporating Fuzzy Lo gic.Proc. 9 th IJCAI, Lo s Angeles (19 85), 70 1{ 703 . 28 F.Kla w onn&R. Krus e [1 4] F.Kla w onn,Prol ogExt ensi on stoM an y{V aluedLogics. In:U .H ohle , E.P .Kl em en t(e ds .),P roc.14t hLinzSe m i nar on FuzzySe tThe ory : Non{Cla ssic al Logi csandthe irA pplica ti on s.Johanne sKeple rUniversit at,Li nz(1992),42{4 5. [ 15]F. Klaw onn,J.Ge bhardt,R.Kruse, Lo gi calApproac hestoU ncertaint y an dV aguenessi ntheVie wof theC on te xtMode l.Proc .IEEE In ternati onalConferenc eonF uzzySy ste m s1992,I EEE, SanDi ego(1992), 1375{13 82 . [ 16]F.Kla w onn,J.Gebhardt,R.K ruse ,TheCon text Mo de lfr omtheV ie wpoin tofLogic.I n:K.{W.H ansm ann,A.B ac hem, M.Jark e ,W. E. Katzen be rger,A.Maruse v,Operations Researc hProc eedi ngs1992. Springer{V erl ag,B erlin( 19 93 ),288{295. [ 17]R.Kruse ,J.Gebhardt,F.Kla w onn,F oundationsofF uzz ySyste m s. Wil ey ,Chi c heste r(1994 ). [ 18]R.Kruse ,E.Sc h w ec k e ,J.He insohn,Unce rta i n t yandV ague nessin Kno wledgeBasedSystem s:Num e ricalM ethods.Springer{V e rlag, Berl in (1991). [ 19] R.C. T.Lee,F uzz yLogi candtheR e soluti onPrinci ple.Journ. ofthe Associ ati on forCom puti ngMac hi nery19 (1972),109{119. [2 0] J.W.Llo yd,F oundations of Lo gicProgram m i ng(2nded.). Spri nge r{ V e rlag,Berl in(198 7) . [ 21]T.P. Ma rtin,J. F.B al dwin,B .W.Pi lsworth,TheI m ple m en tati on of Fp r olo g {AFuzz yP rologI n te rpre ter.F uzz yS et sa nd Syste m s23 (19 87),119{129. [22] M. M ukai d ono, Z.L. Shen, L . D i ng , F un dam entals of F uzz yPro log. I ntern. Journ. Approxi mate Reaso ni ng 3 (198 9), 179{193. [2 3] D. Mundic i, Ul am Gam es, Lu kasiewi cz Lo gic , and AF C ? {Algebras. Funda m en ta Inform atic ae 18 (1993), 151{161. [24] V. No va k, On theSyn tacti ca{ Sem an tic al Com pl etene s s of Fi rst Order Fuzzy Lo gic,Part I:Syntax and Semantics. Kyb ernetica 2 6 (19 90), 47{ 66. A Luk asie wi czL og ic Ba se dP rolog 29 [25] V.No v ak,OntheSy n tactic a{ Sem an ti calCom pl etenesso fF i rstOrder F uzzyLogi c,Part II :M ai nRe sul ts.Kybernetica2 6( 1990),134{154. [26]J.P a v elk a,OnF uzzy Lo gicI ,II ,III .Zei tsc hr.Math.L og ikGrundl. Mat h.25(197 9),4 5{ 52,119{134,447{464. [27]A.Rose,J.B .Rosser,F ragm en tsofM an y{V aluedStat em en tCalc uli. T rans.Am eri ca nM athem ati calSoci et y87( 1958 ),1{53. [28]B.Scarpell ini , Die Nic h taxiom atisi erbark ei t des unendl ic h w e rtigen Pr adik atenkalk ul sv on Luk asi ewic z.J ou rnalofSym boli cLogi c27(196 2), 159{17 0. [29]L .S om b e,Reasoni ngunde rInc om pl eteInform ationi nArticial In te ll ige nc e.Wi ley, Ne wY ork(1990). [30]S . M.U lam ,Adv en tur esofaMa the m atici an.Sc ribner' s,NewY ork (1976). [31]M.U m ano,F uz zySetProlog. Proc.2ndI FSACongress,T oky o(1987), 750{753.