Well-founded and stationary models of logic progra

Well-FoundedandStationaryModelsofLogicProgramsTeodorC.PrzymusinskiDepartmentofComputerScienceUniversityofCaliforniaRiverside,CA92521([e-mail])?TableofContents1Introduction:::::::::::::::::::::::::::::::12Clark’sPredicateCompletionSemanticsanditsDrawbacks:22.1TheNegativeRecursionProblem:Inconsistency:::::::::42.2ThePositiveRecursionProblem:InsucientExpressibility:::53EliminatingDrawbacksofClark’sSemantics:::::::::::73.1PartialClark’sPredicateCompletionSemantics:::::::::73.2LeastModels:::::::::::::::::::::::::::::83.3PerfectModels::::::::::::::::::::::::::::93.4StableModels::::::::::::::::::::::::::::103.5Well-FoundedModels::::::::::::::::::::::::113.6PartialStableorStationaryModels::::::::::::::::123.7RelationshipsBetweenDierentSemantics::::::::::::124Well-FoundedandStationaryModels:::::::::::::::134.1PartialModels::::::::::::::::::::::::::::134.2LeastPartialModels:::::::::::::::::::::::::174.3TheQuotientOperator:::::::::::::::::::::::194.4Well-FoundedModels::::::::::::::::::::::::214.5StationaryModels::::::::::::::::::::::::::264.6Well-FoundedModelCoincideswiththeSmallestStationaryModel274.7DynamicStratication::::::::::::::::::::::::284.8Non-HerbrandModels::::::::::::::::::::::::314.9RelationshiptoNon-MonotonicFormalisms::::::::::::334.10ProceduralSemantics:SLS-resolution:::::::::::::::355Conclusion::::::::::::::::::::::::::::::::37References:::::::::::::::::::::::::::::::::::37?PartiallysupportedbytheNationalScienceFoundationgrant#IRI-9313061.ToappearintheAnnalsofMathematicsandArticialIntelligence.RevisedonJune6,1994.1IntroductionTheintroductionandsubsequentdevelopmentoftheformalfoundationsoflogicprogramminganddeductivedatabaseshasbeenanoutgrowthandanunques-tionablesuccessofthelogicalapproachtoknowledgerepresentation.Thisap-proachisbasedontheideaofprovidingintelligentmachineswithalogicalspecicationoftheknowledgethattheypossess,thusmakingitindependentofanyparticularimplementation.Consequently,aprecisemeaningorsemanticsmustbeassociatedwithanylogicordatabaseprogramPinordertoprovideitsdeclarativespecication.Declarativesemanticsprovidesamathematicallyprecisedenitionofthemeaningoftheprograminamanner,whichisindependentofproceduralcon-siderations,context-free,andeasytomanipulate,exchangeandreasonabout.Proceduralsemantics,ontheotherhand,usuallyisgivenbyprovidingapro-ceduralmechanismthat,atleastintheoryandperhapsundersomeadditionalassumptions,iscapableofsupplyinganswerstoawideclassofqueries.Theperformanceofsuchamechanism(inparticular,itscorrectness)isevaluatedbycomparingitsbehaviortothespecicationprovidedbythedeclarativesemantics.Withoutaproperdeclarativesemanticstheuserneedsanintimateknowledgeofproceduralaspectsinordertowritecorrectprograms.Findingasuitabledeclarativeorintendedsemanticsisoneofthemostimpor-tantanddicultproblemsinlogicprogramminganddeductivedatabases.Theimportanceofthisproblemstemsfromthedeclarativecharacteroflogicpro-gramsanddeductivedatabases,whereasitsdicultycanbelargelyattributedtothefactthattheredoesnotexistapreciselydenedsetofconditionsthata‘suitable’semanticsshouldsatisfy.Whileallresearchersseemtoagreethatanysemanticsmustreecttheintendedmeaningofaprogramoradatabaseandalsobesuitableformechanicalcomputation,thereisnoagreementastowhichsemanticsbestsatisesthesecriteria.Onething,however,appearstobeclear.Logicprogramsanddeductivedatabasesmustbeaseasytowriteandcomprehendaspossible,freefromexces-siveamountsofexplicitnegativeinformationandasclosetonaturaldiscourseaspossible.Inotherwords,thedeclarativesemanticsofaprogramoradatabasemustbedeterminedmorebyitscommonsensemeaningthanbyitspurelylogicalcontent.Forexample,giventheinformationthat1isanaturalnumberandthatn+1isanaturalnumberifsoisn,weshouldbeabletoderiveanon-monotonicorcommonsenseconclusionthatneither0norMickeyMouseisanaturalnum-ber.Similarly,fromadatabaseofinformationaboutteachingassignments,whichonlyshowsthatJohnteachesPascalandPrologthissemester,itshouldbepos-sibletoreachacommonsenseconclusionthatJohndoesnotteachCalculus.Clearly,noneofthesefactsfollowlogicallyfromourassumptions.AssumingthatalogicprogramPisexpressedinsomelanguageLandisconsideredtobeatheoryinsomelogicLog(e.g.,classicalpredicatelogic,three-valuedlogicorepistemiclogic),thedeclarativesemanticsSEM(P)ofPisthesetofallsentencesinLwhichareconsideredtobetrueaboutP.ItisnaturaltorequirethatSEM(P)beclosedunderlogicalconsequenceinLogandthatitshouldataminimumcontainallsentencesderivablefromPinthegivenlogicLog.However,ingeneral,SEM(P)containsmanymoresentencesdescribingthecommonsenseconsequencesofP.ThesemanticsSEM(P)canbespeciedinvariousways,amongwhichthefollowingtwoaremostcommon.Onethatcanbecalledproof-theoretic,associateswithPitsextensionorcompletionCOMP(P),i.e.,a(niteorinnite)theoryinLextendingP.Forexample,COMP(P)canbeClark’spredicatecompletionofP.AsentenceSisthensaidtobelongtoSEM(P)ifandonlyifitderivable,inthelogicLog,fromthecompletion:COMP(P)j=LogS:AcloselyrelatedmethodofdeningthedeclarativesemanticsSEM(P)ofapro-gramismodel-theoretic.Thesemanticsisdeterminedbychoosin