Eliminating Disjunction from Propositional Logic Programs un

eiter,michael,tompits,stefan￠ Abstract. In general, disjunction is considered to add expressive power to propositional logic programs under stable model semantics, and to enlarge the range of problems which can be expressed. However, from a semantical poi

EliminatingDisjunctionfromPropositionalLogicProgramsunderStableModelPreservation

ThomasEiter,MichaelFink,HansTompits,andStefanWoltran

Institutf¨urInformationssysteme184/3,TechnischeUniversit¨atWien,

Favoritenstraße9-11,A-1040Vienna,Austria

eiter,michael,tompits,stefan@kr.tuwien.ac.at

Abstract.Ingeneral,disjunctionisconsideredtoaddexpressivepowertopropo-sitionallogicprogramsunderstablemodelsemantics,andtoenlargetherangeofproblemswhichcanbeexpressed.However,fromasemanticalpointofview,disjunctionisoftennotreallyneeded,inthatanequivalentprogramwithoutdis-junctioncanbegiven.Wethusconsiderthequestion,givenadisjunctivelogicprogram,doesthereexistanequivalentnormal(i.e.,disjunction-free)logicprogram?Infact,weconsiderthisissuefordifferentnotionsofequivalence,namelyforordinaryequivalence(regardingthecollectionsofallstablemodelsoftheprograms)aswellasforthemorerestrictivenotionsofstronganduniformequivalence.Weresolvetheissueforpropositionalprograms,andpresentasim-ple,appealingsemanticcriterionfortheprogramsfromwhichalldisjunctionscanbeeliminatedunderstrongequivalence;testingthiscriterioniscoNP-complete.Wealsoshowthatunderordinaryanduniformequivalence,thiseliminationisalwayspossible.Inallcases,thereareconstructivemethodstoachievethis.Ourresultsextendandcomplementrecentresultsonsimplifyinglogicprogramsun-derdifferentnotionsofequivalence,andaddtothefoundationsofimprovingimplementationsofAnswerSetSolvers.

1Introduction

Disjunctivelogicprogrammingisanextensiontonormallogicprogrammingwhichisgenerallyconsideredtoaddexpressivepowertologicprogramsunderstablemodelse-mantics,andtoenlargetherangeofproblemswhichcanbeexpressed.Thisviewissupportedbyresultsontheexpressivenessofdisjunctivelogicprograms(DLPs)over nitestructures,whichshowthatpropertiesatthesecondlevelofthePolynomialHi-erarchy(PH)canbeexpressedbyinferencefromfunction-free(Datalog)DLPs[11],whilebynormallogicprogramsonlypropertiesatthe rstlevelcanbeexpressed[28].However,fromasemanticalpointofview,disjunctionisoftennotreallyneeded,inthatanequivalentnormallogicprogram(NLP,i.e.,withoutdisjunction)canbegiven.Forexample,in[10],itwasshownthatinthepresenceoffunctionssymbols,DLPshaveoverHerbrandmodelsthesameexpressivepowerasNLPs,namely.

WiththeriseofAnswerSetProgrammingasaprogramsolvingparadigm,inwhichsolutionsarecomputedintheanswersetsresp.stablemodelsofalogicprogram,at-tentionhasbeendirectedtotheexpressivenessoflogicprogramsintermsofthewhole

eiter,michael,tompits,stefan￠ Abstract. In general, disjunction is considered to add expressive power to propositional logic programs under stable model semantics, and to enlarge the range of problems which can be expressed. However, from a semantical poi

152ThomasEiteretal.

collectionoftheiranswersetsperseratherthantheirintersection(resp.union)asincautiousandbravereasoning,respectively),cf.[20];relatedtothisispreliminaryworkontheexpressivenessofformalismssuchasdefaultlogicandcircumscription[13,19].

Inparticular,equivalenceoflogicprogramsintermsoftheircollectionsofstablemodelshasbeenconsidered,aswellasthere nednotionsofstrongequivalence,cf.

[16,29,30,24,17,4],anduniformequivalence[7,8,25],whichdatesbackto[27,18].

andarestronglyequivalent(resp.,uniformlyequivalent),if,foranyTwoDLPs

setofrules(resp.,setofatoms),theprogramsandareequivalentunderthestablesemantics,i.e.,havethesamesetofstablemodels.

Stronganduniformequivalencecanbeutilizedforprogramoptimization,cf.[30,22,8],takingintoaccountpossibleincompletenessofaprogram,wherenotallrulesareknownatthetimeofoptimization,respectivelyvaryinginputdatagivenbyatomicfactsarerespected.Thisisinparticularhelpfulforoptimizingcomponentswhichareembeddedintoamorecomplexlogicprogram.NotethatasrecentlydiscussedbyPearceandValverde[25],uniformandstrongequivalenceareessentiallytheonlyconceptsofequivalenceobtainedbyvaryingthelogicalformoftheprogramextensions.

Anaturalissueinthiscontextistheexpressivenessofdisjunctioninruleheads,i.e.,whetheritreallyaddsexpressivepower.Thisisindeedthecase,ascanbeseenonthesimpleexampleoftheprogram:Thisprogramisnotstronglyequivalenttoanynormallogicprogram(cf.[30]).However,aseasilyseenisequivalenttotheNLPsinceforboththestablemodelsareand,andfurthermoreisalsouniformlyequivalentto(thisisimmediatefromtheresultthatrewritingahead-cyclefreeprogramtoanormallogicprogrambystandardshiftingpreservesuniformequivalence[7]).Ontheotherhand,theenrichedprogramisstronglyequivalenttotheprogram.Thisraisesthequestionofacriterionwhichtellswhendisjunctionscanbeelimi-nated,andamethodfordeciding,givenadisjunctivelogicprogram,doesthereexistanequivalentnormal(i.e.,disjunction-free)program?Westudythisissueforpropo-sitionalprograms,onwhichwefocushere,andmakethefollowingcontributions:

–Wepresentasimple,appealingsemanticcharacterizationoftheprogramsfromwhichalldisjunctionscanbeeliminatedunderstrongequivalence.Thecharac-terizationisbasedonthestrong-equivalencemodels(SE-models)[29,30]whichrephrasemodelsinthemoregenerallogicofhere-and-there[16]inlogicprogram-mingterms.Infact,weshowthatthispropertyholdsforaprogramifandonlyifthecollectionofSE-modelsofisclosedunderhere-intersection,i.e.,wheneverandareSE-modelsof,thenalsoisanSE-modelof.Inmorefamiliarterms,thisconditionisequivalenttotheprop-ertythatforeachclassicalmodelof,theGelfond-LifschitzreductofissemanticallyHornifmodelsnotcontainedinaredisregarded.–Wefurthershowthatunderordinaryanduniformequivalence,thiseliminationisalwayspossible.Inallthreecases,weobtainaconstructivemethodtorewriteaDLPtoanequivalentnormallogicprogram.Ingeneral,therewritingwillbeofexponentialsize(ifitexists),butthiswillbeunavoidableinpractice.

–Finally,weshowthattestingwhetherf …… 此处隐藏：32422字，全部文档内容请下载后查看。喜欢就下载吧 ……