Contents Debugging in Logic Programming Declarat

DebuggingofLogicProgramsundertheAnswer-SetSemanticsJ¨orgP¨uhrer184.259-Seminarf¨urDiplomandInnenfirsttalk-scopeofmaster’sthesisContentsäContextäTypesofErrors(inASP)äDebugginginLogicProgrammingäDeclarativeErrorDiagnosisäExistingApproachesäWorkinProgress1Contextäanswer-setprogramming(ASP)–promisingapproachfordeclarativeproblemsolving–efficientsolverimplementations(DLV,Smodels)äHowever,–writinglargeanswer-setprogramsiscomplicated–nosupporttoolsforprogrammers–methodologiesprovidinganalysisanddebuggingofanswer-setprogramsaredesirable2TypesofErrorsäErrorcategoriesbylevelofspecification:–lexicallevel:stringsdonotoccurintheprogramminglanguage–syntacticlevel:stringsarecorrect,butdonotmatchsyntaxoftheprogramminglanguage–semanticlevel:syntaxcorrect,buttheprogramdoesn’tmakesense–conceptuallevel:theprogramiscorrectbutdoesn’tservetheintendedpurpose3TypesofErrorsinASPäErrorsinASP:–lexicalandsyntacticlevel:∗errorsaretrivial∗mightbetedious-noneedforidentifierdeclaration–semanticlevel:noerrorsonsemanticlevel-syntacticallycorrectprogramshavewelldefinedsemantics–conceptuallevel:answersetsdonotmeetexpectations4DebuggingStrategiesinLogicProgrammingäTracingProgrammer...–isfamiliarwithbackgroundsearchprocedure–tracesthesolvingalgorithm–mayinfluencetheevolutionoftheproofsearchtree–setsbreakpoints/spypointsäProminentexample:TracinginProlog5DebuggingStrategiesinLogicProgramming(ctd.)äTracinginASP?–restrictiononsolvingalgorithm:intermediateresultsmustbeuseful–hugeamountofunrelevantinformation–notveryelegant(doesnotmeetthedeclarativenatureofASP)älookingfordeclarativedebuggingstrategieshidingtheconstructionofanswer-sets6DeclarativeErrorDiagnosisädeclarativeerrordiagnosis-introducedin1982byShapiro–assumption:programmerhasclearexpectationsabouttheoutcomeofaprogram–informationusedasanoracleäbehaviourofadeclarativediagnosersystem:–input:expectedresults,actualresults,failingprogram–output:informationaboutbug(location,typeofbug,hintsetc.)7DeclarativeErrorDiagnosis(ctd.)ädeclarativeerrordiagnosisforanswer-setprogramming–expectedresult:∗aspecificsetofanswersetsädebugginginformation:–WhyissetSofliteralsinanswersetA?–WhyissetSofliteralsnotinanyanswerset?–Whyisn’tthereanyanswerset?8ExistingApproaches-MartinBrain,MarinaDeVosäAlgorithm:WhyissetSofliteralscontainedinAnswerSetA?äUnderwhichcircumstancesdoesanatomaoccurinanswersetA?äTheremustberuleswhichsupporta.äAtleastoneoftheserulesmustbeapplicableforanswersetA.äUnderwhichcircumstancesdoesanatombnotoccurinanswersetA?äRuleswhichsupportbmustnotbeapplicable.9ExistingApproaches-Brain,DeVos(ctd.)äAlgorithm:WhyissetSofliteralscontainedinAnswerSetA?äcaseatomb∈S:äfindrulessupportingbwhichareapplicableunderAäAnswer:biscontainedinAbecauserulersupportsbäcase(notb)∈S:äfindrulessupportingbäAnswer:bisnotcontainedinAbecausebisnotsupportedbyanyruleäAnswer:bisnotcontainedinAbecausethebodiesofallrulessupportingbarenotcontainedinA10ExistingApproaches-Brain,DeVos(ctd.)äAlgorithm:WhyissetSofliteralscontainedinAnswerSetA?äexample:P={a←b.,c←notd,a.,d←notc,a.,b.}AS(P)={{a,b,c},{a,b,d}}S={a,notd}WhyisScontainedin{a,b,c}?äaisin{a,b,c}becauserulea←b.isapplied.ädisnotin{a,b,c}asonlyruled←notc,a.supportsdbutcisintheanswerset.11ExistingApproaches-Brain,DeVos(ctd.)äAlgorithm:WhyissetSofliteralsnotcontainedinanyAnswerSet?äReasonswhyasetSofliteralsisnotcontainedinanyanswerset:äThereisanatoma∈Swhichisnotsupportedbyanyrules.äTheelementsofSleadtoacontradiction.äTheelementsofSrequiremutuallyinconsistentconditions.12ExistingApproaches-Brain,DeVos(ctd.)äAlgorithm:WhyissetSofliteralsnotcontainedinanyAnswerSet?äBuildalabeleddirectedacyclicgraphG:änodes:Atoms,verum,falsumäedges:positiveresp.negativesupportrelationänoedgesinthebeginningäaddingedgefailsifloopwouldbeintroducedäaddingnegativeedgefailsfromstart-nodesofpositiveedgesorviceversaäCheckifSdirectlyleadstoacontradictionbyaddingedgesforallrulesapplicableforSäCreateconsistentsituations(setsofliterals)basedonGbyaddingedgesforrulessupportingS13ExistingApproaches-Brain,DeVos(ctd.)r1:a←notb,cr2:b←notar3:c←notdr4:e←cr5:e←dr6:f←c,notdr7:g←noth,er8:h←notg⊺⊥abcdefghäAS(P)={{a,c,e,f,g},{a,c,e,f,h},{c,b,e,f,g},{c,b,e,f,h}}äWhyisS={a,b,c}notcontainedinanyAnswerSet?14ExistingApproaches-Brain,DeVos(ctd.)äWhyisS={a,b,c}notcontainedinanyAnswerSet?r1:a←notb,cr2:b←notar3:c←notdr4:e←cr5:e←dr6:f←c,notdr7:g←noth,er8:h←notg⊺⊥abcdefgh-äAS(P)={{a,c,e,f,g},{a,c,e,f,h},{c,b,e,f,g},{c,b,e,f,h}}15ExistingApproaches-Brain,DeVos(ctd.)äWhyisS={a,b,c}notcontainedinanyAnswerSet?r1:a←notb,cr2:b←notar3:c←notdr4:e←cr5:e←dr6:f←c,notdr7:g←noth,er8:h←notg⊺⊥abcdefgh-+äAS(P)={{a,c,e,f,g},{a,c,e,f,h},{c,b,e,f,g},{c,b,e,f,h}}16ExistingApproaches-Brain,DeVos(ctd.)äWhyisS={a,b,c}notcontainedinanyAnswerSet?r1:a←notb,cr2:b←notar3:c←notdr4:e←cr5:e←dr6:f←c,notdr7:g←noth,er8:h←notg⊺⊥abcdefgh-++-äAS(P)={{a,c,e,f,g},{a,c,e,f,h},{c,b,e,f,g},{c,b,e,f,h}}17ExistingApproaches-Brain,DeVos(ctd.)äWhyisS={a,b,c}notcontainedinanyAnswerSet?r1:a←notb,cr2:b←notar3:c←notdr4:e←cr5:e←dr6:f←c,notdr7:g←noth,er8:h←notg⊺⊥abcdefgh-++--äAS(P)={{a,c,e,f,g},{a,c,e,f,h},{