Stable models and an alternative logic programming

arXiv:cs.LO/9809032v118Sep1998StablemodelsandanalternativelogicprogrammingparadigmVictorW.Marek,MiroslawTruszczynskiDepartmentofComputerScienceUniversityofKentuckyLexington,KY40506-0046{marek,mirek}@cs.engr.uky.eduAbstractInthispaperwereexaminetheplaceandroleofstablemodelsemanticsinlogicpro-grammingandcontrastitwithaleastHerbrandmodelapproachtoHornprograms.Wedemonstratethatinherentfeaturesofstablemodelsemanticsnaturallyleadtoalogicpro-grammingsystemthatoffersaninterestingalternativetomoretraditionallogicprogram-mingstylesofHornlogicprogramming,stratifiedlogicprogrammingandlogicprogram-mingwithwell-foundedsemantics.Theproposedapproachisbasedontheinterpretationofprogramclausesasconstraints.Inthissettingprogramsdonotdescribeasinglein-tendedmodel,butafamilyofstablemodels.Thesestablemodelsencodesolutionstotheconstraintsatisfactionproblemdescribedbytheprogram.Ourapproachimposesre-strictionsonthesyntaxoflogicprograms.Inparticular,functionsymbolsareeliminatedfromthelanguage.Wearguethattheresultinglogicprogrammingsystemiswell-attunedtoproblemsintheclassNP,hasawell-defineddomainofapplications,andanemergingmethodologyofprogramming.Wepointoutthatwhatmakesthewholeapproachviableisrecentprogressinimplementationsofalgorithmstocomputestablemodelsofpropositionallogicprograms.1IntroductionStablemodelsemanticsappearedonthelogicprogrammingsceneinthelate80sinanefforttoprovideanunderstandingofprogramswithnegation.SinceitwasfirstproposedbyGelfondandLifschitz[GL88],itwasregardedbylogicprogrammingcommunitywithadoseofreserveandunease.Itwasintuitivelyfeltthatthestablemodelsemanticsproperlydealswithnegationandsomeformalevidencesupportingthisintuitionwasestablished.Atthesametime,thestablemodelsemanticsdidnotfitintoastandardparadigmoflogicprogramminglanguages.Whilestandardapproachesassigntoalogicprogramasingle“intended”model,stablemodelsemanticsassignstoaprogramafamily(possiblyempty)of“intended”models.Further,inthepresenceoffunctionsymbols,Hornlogicprogramscanspecifyanyrecursivelyenumerableset,whilestablemodelsemanticsincreasestheexpressivepoweroflogicprogramswellbeyond1acceptablenotionsofcomputability.Finally,theSLD-resolution,thetruebread-and-butteroflogicprogrammersandtheheartofcontrolmechanismsbehindstandardlogicprogrammingimplementations,seemstobeinappropriateforthestablemodelsemantics.Asaconsequenceofthesedifficultiesinreconcilingthestablemodelsemanticswithatra-ditionalparadigmoflogicprogramming,thestablemodelsemanticsreceivedrelativelylessattentionfromthelogicprogrammingcommunitythanothersemanticsproposedforprogramswithnegationsuchasperfectmodelsemanticsforstratifiedprogramsandwellfoundedseman-tics.Inthispaperwearguethatratherthantotrytoresolvetheseinconsistenciesandforcestablemodelsemanticsintoastandardlogicprogrammingmold(thiseffortmostlikelyisdoomedtofailure),achangeofviewisrequired.Therefore,weproposeaperspectiveonthestablemodelsemanticsthatdepartsfromseveralbasictenetsoflogicprogramming.Atthesametime,thisperspectiveleadstoacomputationalsystemverymuchinthegeneralspiritoflogicprogramming.Thesystemisdeclarative,retainstheseparationoflogicfromcontrol,hasawell-defineddomainofapplicationsandemergingprogrammingmethodology.Werefertothisversionoflogicprogrammingasstablelogicprogramming(or,SLP,forshort).Thereareseveralkeyelementstotheviewonthestablemodelsemanticsthatwedescribehere.First,werestrictthesyntaxbydisallowingfunctionsymbols.Thus,thesyntaxofSLPisthesameasthesyntaxofDATALOGwithnegation.Therestrictionofthesyntaxhassignificanteffectontheexpressivepowerofprograms.Inparticular,itcurtailstheabilitytouserecursion.Second,weviewaprogramasspecifyingacollectionofmodelsratherthanasinglemodel.Thus,SLPseemstobeespeciallywellsuitedforalltheseproblemswheresolutionsaresub-setsofsomeuniverse,aseachsolutioncanbemodeledbyadifferentstablemodel.Manycombinatorialandconstraintsatisfactionproblemsfallintothiscategory.Therestrictedsyntax(limitingtheuseofrecursion)andtheshiftinthesemantics(programsspecifyacollectionofmodelsratherthanasinglemodel),changethewayinwhichweinterpretanddesignprograms.Programsareinterpretedassetsofconstraints.Clausesrepresentindividualconstraintsonobjectsofinterestratherthanrecursivedefinitionsoftheseobjects.Hence,adifferentapproachtoprogrammingisneeded.ObjectsthatinHornlogicprogrammingwouldberepresentedastermsanddefinedrecursively,inSLParerepresentedasdifferentstablemodelsanddefinedintermsofconstraints.Finally,althoughtheSLPfollowsthebasiclogicprogrammingtenetof“uniformcontrol”,thecontrolusedinSLPisdifferent.InsteadofSLDresolutionusedinHornLogicprogramming,abacktrackingsearchforstablemodelsisused.While(Horn)logicprogrammingiswellattunedtotheconceptsofTuringcomputability,recursivelyenumerablesetsandpartialrecursivefunctions,SLPisrelatedtoamuchmorenarrowclassofproblems.Aswepointout,alldecisionproblemsthatareinNPcanbesolvedwithintheparadigmofSLP.Moreovermany(possiblyall)searchproblems,whosedecisionversionsareinNP,canbesolvedwithSLPprograms,too.WhileNPismuchsmallerthantheclassofr.e.sets,itstillcoversawidecollectionofimportantcomputationalproblemsincl