Foundations of Disjunctive Logic Programming

TheoryofDisjunctiveLogicProgramsJackMinker(1;2)ArcotRajasekar(1)JorgeLobo(1)DepartmentofComputerScience(1)andInstituteforAdvancedComputerStudies(2)UniversityofMarylandCollegePark,Maryland207421IntroductionTheadventoftheageofmoderncomputers,hasseenanincreasedinterestinautomatinglogicaldeduction.Inthelate1950’sproceduresformechanicaltheoremprovingwerede-velopedand/orimplementedbyDavisandPutnam[DP60],Gilmore[Gil60]andPrawitz[Pra60]forsolvingproblemsencodedinrstorderlogic.Theseeortswerethebeginningofthemoderneldofautomatedtheoremprovingbydigitalcomputers.InterestinthisareaacceleratedwiththepublicationofapaperbyRobinson[Rob65]inwhichhedescribestheResolutionPrinciple.Robinson’smethodofperformingautomateddeductionisawater-shedinautomatedtheoremprovingbecauseitprovidesasinglesoundandcompleteruleofinferenceforrst-orderlogic.Subsequentdevelopmentsinautomatedtheoremprov-inghaverevolvedaroundtheRobinsonresolutionprincipleandseveralrenementssuchastheset-of-support,linearrenement,model-eliminationandotherstrategieshavebeendeveloped.ChangandLee[CL73]andLoveland[Lov78]provideindepthstudiesoftheprocedureswhichweredevelopedintheyearsimmediatelyfollowingRobinson’slandmarkpaper[Rob65].Animportantdevelopmentleadingfromautomatedtheoremprovingistheeldoflogicprogramming.Thecentralideainthisdevelopmentisthatlogiccanbeusedasaprogram-minglanguage.ColmerauerandKowalskiwerethersttorealizethisnewinterpretationforlogic.Independently,Elcock[Elc88],Green[Gre69]andHewitt[Hew69]appliedsimilarideasandtechniquesintheirresearch.Colmeraueret.al.[CKPR73]implementedtherstlogicprogrammingsystem,calledPROLOG(PROgrammationenLOGique)whichwasusedfornaturallanguagequestionanswering.Kowalski[Kow74]showedthatlogicrestrictedtoHornclausesprovidesaconvenientframeworkforaprogramminglanguage.Untilthen,logicwasconsideredonlytobeaspecicationlanguageincomputerscience.Thenewinterpretationforlogic,providedbyKowalski,showingthatlogichasaproceduralmeaning,wasrevolutionaryandreducedtheconceptofdeduction(inHornclauses)toaconceptofproceduralinterpretation.Thetasksofsubstitutionandunicationcapture,respectively,parameterpassingandprocedurecallsofconventionalprogramexecution.ThisworkwassupportedbytheNationalScienceFoundationundergrantnumberIRI-86-09170andtheArmyResearchOceundergrantnumberDAAG-29-85-K-0-177.1Researchinlogicprogramminghasproceededinthreedirections:theory,implementa-tionandapplications.Studiesresultinginthedevelopmentofdeclarativesemanticsandinthecharacterizationoftheoriesandrulesofnegationcontinuetoprovidearichtheoreticalframeworkforlogicprograms.EcientimplementationofPROLOGsystems,basedontheproceduralinterpretationofHornlogicprograms,havebeeninstrumentalinhelpinglogicprogramminggainwideacceptanceinthearticialintelligenceanddatabasecommunities.Logicprogramsarendingincreaseduseinapplicationsrangingfromnaturallanguageprocessingtoexpertsystemstoproblemsinnonmonotonicreasoning.Untilrecently,themajorthrustintheuseoflogicasaprogramminglanguagehasbeenintheareaofHornlogicprograms,usingwhatarecalleddeniteprogramclauses.vanEmdenandKowalski[vEK76]provideddeclarativeandproceduralsemanticsforHornprograms.Apt,BlairandWalker[ABW88]andVanGelder[Van88]developeddeclarativesemanticsforstratiedHornprograms.Recently,VanGelder,RossandSchlipf[VRS88]usedthree-valuedmodelstodenesemanticsforgeneralHornprograms.Inthispaper,weextendthetheoreticalresultsachievedinHornlogicprograms,toincludewhatwecalldisjunctivelogicprograms,whichdealwithindeniteprogramclauses.ThemotivationforthepaperistodenesemanticsforlogicprogramswhichextendtheHorn(atomic)frameworktodealwithindenite(clausal)information.ThesyntacticsimilarityofdisjunctiveprogramsandHornprogramsandtheexistenceofcoherentsemanticsforHornprogramsprovidestherequiredvehicleandmotivationtodenesemanticsfordisjunctiveprograms.Deningsuchasemanticswouldhelpgaininsightintotheuseofindeniteinformationasaviabledata-structure(null-valueproblemandnon-stratiableprogramsareexampleswheretheuseofindeniteinformationmightbeneeded.)Studyingthesemanticsofdisjunctiveprogramsmightalsobehelpfulindevelopingnewprogrammingtoolsandprocedures.Theaimofthepaperistoprovideatheoreticalfoundationfordisjunctiveprogramswiththeintentofmotivatingtheuseofdisjunctivetheoriesasaviableprogramminglanguage.Westudythesemanticsofdisjunctivelogicprogramsanddevelopdeclarativeandpro-ceduralsemantics.Westudythedeclarativesemanticsofdisjunctivelogicprogramsusingxpointsemantics,modeltheoryandtheoriesofnegation.Proceduralinterpretationsaredevelopedtodescribequeryansweringproceduresforhandlingbothpositiveandnegativequeriesindisjunctivelogicprograms.Wealsoprovidedeclarativesemanticsforgeneraldisjunctivelogicprograms.ThesemanticsextendsthesemanticsofHornandgeneralHornlogicprogramsdescribedin[vEK76,AvE82,Hil74,Cla78,Rei78].Thesemanticsalsopro-videsadierentcharacterizationoftheworkfoundin[Min82,RT88,Prz86].Table1attheendofthepapersummarizestheworkpresentedherejuxtaposedwithrelevantworkdonepreviouslybyotherresearchers.Thematerialpresentedinthispaperhasbeendrawnfromase