Reasoning
YannisDimopoulos
UniversityofCyprusDept.ofComputerScienceyannis@cs.ucy.ac.cy
BernhardNebel
Universit¨atFreiburgInstitutf¨urInformatiknebel@uni-freiburg.de
FrancescaToni
ImperialCollegeDept.ofComputingft@doc.ic.ac.uk
Abstract
Bondarenkoetal.haverecentlyproposedanabstractframeworkfor
defaultreasoning.Besidescapturingmostexistingformalismsandprov-ingthattheirstandardsemanticsallcoincide,theframeworkextendstheseformalismsbygeneralisingthesemanticsofadmissibleandpreferredargu-ments,originallyproposedforlogicprogrammingonly.
Inthispaperweanalysethecomputationalcomplexityofcredulousandscepticalreasoningunderthesemanticsofadmissibleandpreferredargu-mentsfor(thepropositionalvariantof)theinstancesoftheabstractframe-workcapturingtheorist,circumscription,logicprogramming,defaultlogic,andautoepistemiclogic.Althoughthenewsemanticshavebeentacitlyas-sumedtomitigatethecomputationalhardnessofdefaultreasoningunderthestandardsemanticsofstableextensions,weshowthatinmanycasesreason-ingundertheadmissibilityandpreferabilitysemanticsiscomputationallyharderthanunderthestandardsemantics.Inparticular,inthecaseofau-toepistemiclogic,scepticalreasoningunderpreferredargumentsislocatedatthefourthlevelofthepolynomialhierarchy,whereasthesameformofreasoningunderstableextensionsislocatedatthesecondlevel.
1
1Introduction
Bondarenkoetal.[1]showthatmanylogicsfordefaultreasoning,i.e.,theorist[25],(manycasesof)circumscription[20],DefaultLogic(DL)[26],Nonmono-tonicModalLogic[21],AutoepistemicLogic(AEL)[22],andLogicProgram-ming(LP)canbeunderstoodasspecialcasesofasingleabstractframework.Thestandardsemanticsofalltheselogicscanbeunderstoodassanctioningasetofassumptionsasastableextensionofagiventheory,formulatedinanunderlyingmonotoniclogic,iffthesetofassumptionsdoesnotattackitselfanditattackseveryassumptionnotintheset.Inabstractterms,anassumptioncanbeattackedifitscontrarycanbeproved,intheunderlyingmonotoniclogic,possiblywiththeaidofotherconflictingassumptions.
Bondarenkoetal.alsoproposetwonewsemanticsgeneralising,respectively,theadmissibilitysemantics[8]andthesemanticsofpreferredextensions[8]orpartialstablemodels[27]forLP.Inabstractterms,asetofassumptionsisanadmissibleargumentofagiventheory,formulatedinanunderlyingmonotoniclogic,iffitdoesnotattackitselfanditattacksallsetsofassumptionswhichattackit.Asetofassumptionsisapreferredargumentiffitisamaximal(withrespecttosetinclusion)admissibleargument.
Thenewsemanticsaremoregeneralthanthestabilitysemanticssinceeverystableextensionisapreferred(andadmissible)argument,butnoteverypreferredargumentisastableextension.Moreover,thenewsemanticsaremoreliberalbecauseformostconcretelogicsfordefaultreasoning,admissibleandpreferredargumentsarealwaysguaranteedtoexist,whereasstableextensionsarenot.Fi-nally,reasoningunderthenewsemanticsappearstobecomputationallyeasierthanreasoningunderthestabilitysemantics.Intuitively,toshowthatagivensen-tenceisjustifiedbyastableextension,itisnecessarytoperformaglobalsearchamongstalltheassumptions,todetermineforeachsuchassumptionwhetheritoritscontrarycanbederived,independentlyofthesentencetobejustified.Forthesemanticsofadmissibleandpreferredarguments,however,a“local”searchsuffices.First,onehastoconstructasetofassumptionswhich,togetherwiththegiventheory,(monotonically)derivesthesentencetobejustified,andthenonehastoaugmenttheconstructedsetwithfurtherassumptionstodefenditagainstallattacks[18,6,7].
However,fromacomplexity-theoreticpointofview,itseemsunlikelythatthenewsemanticsleadtobetterlowerboundsthanthestandardsemanticssinceallthe“sourcesofcomplexity”onehasindefaultreasoningarestillpresent.Therearepotentiallyexponentiallymanyassumptionsetssanctionedbythesemantics.Further,inordertotestwhetherasentenceisentailedbyaparticularargument,onehastoreasonintheunderlyingmonotoniclogic.Forthisreason,onewouldexpectthatreasoningunderthenewsemanticshasthesamecomplexityasunderthestabilitysemantics,i.e.,itiscompleteforthefirstlevelofthepolynomialhierarchyforLPandonthesecondlevelforlogicswithfullpropositionallogicastheunderlyinglogic[3].However,previousresultsontheexpressivepowerofDATALOGqueriesbySacc`a[28]suggestthatthisisnotthecaseforLP.Indeed,Sacc`a’sresultsimplythatreasoningunderthepreferabilitysemanticsforLPisatthesecondlevelofthepolynomialhierarchy.
Inthispaperweextendthisanalysisandprovidecomplexityresultsforrea-soninginthepropositionalvariantsoftheorist,circumscription,LP,DL,andAELunderthenewsemantics.Asitturnsout,reasoningunderthenewsemanticscanbemuchharderthanreasoningunderthestandardsemantics.Inparticular,weshowthatscepticalreasoninginDLunderthepreferabilitysemanticsisonthethirdlevelofthepolynomialhierarchy,thatcredulousreasoninginAELundertheadmissibilitysemanticsisonthethirdlevelofthepolynomialhierarchy,andthatscepticalreasoninginAELunderthepreferabilitysemanticsisonthefourthlevelofthepolynomialhierarchy.
Thepaperisorganisedasfollows.Section2summarisesrelevantfeaturesoftheabstractframeworkof[1],itssemanticsandconcreteinstances.Section3givescomplexitytheorybackgroundandintroducesthereasoningproblems.Sec-tion4givesgenericupperboundsforcredulousandscepticalreasoning,para-metricwithrespecttothecomplexityoftheunderlyingmonotoniclogics.Thegenericresultsareinstantiatedtoprovideupperboundsforconcreteinstancesoftheabstractframework.Section5givesthencompletenessresultsfortheoristandcircumscription,Section6givesthecompletenessresultsforLPandDL,andSec-tion7givesthecompletenessresultsforAEL.Section8discussestheresultsandconcludes.
2DefaultReasoningviaArgumentation
issomeformallanguagewithAssumeadeductivesystem(,),where
countablymanysentencesandisasetofinferencerulesinducingamono-andaformula,tonicderivabilitynotion.Givenatheory
isthedeductiveclosureof.Then,anabstract
(assumption-based)frameworkisatripleisamappingfrominto.,thetheory,isasetofbeliefs,formulatedintheun-derlyinglanguage,andcanbeextendedbysubsetsof,thesetofassumptions.Indeed,anextensionofanabstractframework
denotesthecontraryof.
Theoristcanbeunderstoodasaframework
ability.
Manycasesofcircumscriptioncanbeunderstoodsimilarly,exceptthattheassumptionsarenegationsofatomicsentences,forallpredicateswhichareminimised,andatomicsentencesortheirnegations,forallpredicateswhicharefixed.
LPistheinstanceoftheabstractframework
ofanassumption
isjustitsnegation.
isordinaryclassicalprov-
ofanassumptionis.isHornlogicprovability,withassump-tions,,understoodasnewatoms,asin[12].DListheinstanceoftheabstractframework
wherearesentencesinclassicallogic.isaclassicaltheoryandconsistsofallexpressionsoftheformwhereisasentenceofclassicallogic.Thecontrary
Namely,allcaseswhereeverymodelofthetheorytobecircumscribedisaHerbrandmodelofthetheory,see[1]formoredetails.
4
Givenanabstractframework
;
attacksanassumptionset.
iff
attackssomeassumption
isclosediff,Giventhatanassumptionset
thestandardsemanticsofextensionsoftheorist[25],minimalmodelsofcircum-scription[20],extensionsofDL[26],stableexpansionsofAEL[22],andstablemodelsofLP[14]correspondtothestabilitysemanticsofabstractframeworks,whereanassumptionsetisstableiff
1.2.3.
isclosed,
doesnotattackitself,andattackseachassumption
.
AssumptionsetsarealwaysclosedinthecaseofLPandDL.Frameworkswiththispropertyarereferredtoasflat[1].Assumptionsetsmightnotbeclosed
inAEL,theinthecaseofAEL.Forexample,giventhetheory
emptyassumptionsetisnotclosed.Furthermore,assumptionsetsmightnotbeclosedinthecaseoftheoristandcircumscription.Forexample,ifaformulaisanassumptionintheoristthatisalreadyderivedbythetheory,thentheemptyassumptionsetisnotclosed.
Astableextensionisanextensionforsomestableassumptionset.Thestandardsemanticsofcircumscription[20]correspondstotheintersectionofallstableextensionsoftheabstractframeworkcorrespondingtocircumscrip-tion.
Bondarenkoetal.arguethatthestabilitysemanticsisunnecessarilyrestric-tive,becauseitinsiststhatanassumptionsetshouldtakeastandoneveryissue(assumption).Thus,theydefinenewsemanticsfortheabstractframework,bygeneralisingtheargumentation-theoreticreformulationof[17]forthesemanticsoriginallyproposedforLPbyDung[8].Thenewsemanticsaredefinedintermsof“admissible”and“preferred”setsofassumptions/extensions.Anassumptionsetisadmissibleiff
1.
isclosed,
5
2.
doesnotattackitself,and
3.forallclosedsetsofassumptions
.
,if
attacks
then
attacks
Maximal(withrespecttosetinclusion)admissibleassumptionsetsarecalledpreferred.Inthispaperweusethefollowingterminology:anadmissible(pre-forsomeadmissible(preferred)ferred)argumentisanextension
assumptionset.Bondarenkoetal.showthatpreferredargumentscorrespondtopreferredextensions[8]andpartialstablemodels[27]forLP.
Everystableassumptionset/extensionispreferred(andthusadmissible)[1,Theorem4.6],butnotviceversa,ingeneral.However,iftheframeworkisnor-mal,i.e.,ifeverymaximalclosedassumptionsetthatdoesnotattackitselfisastableset,thenthesemanticsofpreferredandstableassumptionsetscoincide[1,Theorem4.8].Theoristandcircumscriptionarenormalframeworks,whichimpliesthatstabilityandpreferabilitysemanticsareidenticalinthesecases.Inthesequelwewillusethefollowing:
(Prop):Everypreferredassumptionsetis(trivially)admissibleandeveryad-missibleassumptionsetisasubsetofsomepreferredassumptionset;
(Prop):Theemptyassumptionsetisalwaysadmissible,trivially,forallflat
frameworks;
(Prop):Everypreferredextensionisstableandeverystableextensionispre-ferred,forallnormalframeworks.
Moreover,foranygivensemanticsamongstthestability,admissibilityandpreferabilitysemantics,wewillusetheterminologythat“asetofassumptionsis
sanctionedbyasemantics”tomeanthatthesetofassumptionsisstable/admissible/preferred,respectively.
3
ReasoningProblemsandComputationalComplex-ity
Wewillanalysethecomputationalcomplexityofthefollowingreasoningprob-lemsforthepropositionalvariantsoftheframeworksfortheorist,circumscription,LP,DL,andAELunderadmissibilityandpreferabilitysemantics:
6
thecredulousreasoningproblem,i.e.,theproblemofdecidingforany
whetherforsomeassumptionsetgivensentence
sanctionedbythesemantics;
thescepticalreasoningproblem,i.e.,theproblemofdecidingforanygivensentencewhetherforallassumptionsetssanctionedbythesemantics.
Insteadofthescepticalreasoningproblem,wewilloftenconsideritscomplemen-taryproblem,i.e.
theco-scepticalreasoningproblem,i.e,theproblemofdecidingforanygivensentencewhetherforsomeassumptionsetsanctionedbythesemantics.
Notethatwearenotadvocatingco-scepticalreasoningasinterestingorusefulepistemologically.Rather,weuseittosupportourcomplexityanalysis.
Inaddition,wewillconsiderasub-problemofalltheseproblems,namely:
theassumptionsetverificationproblem,i.e.,theproblemofdecidingwhetheragivensetofassumptionsissanctionedbythesemantics.
Webrieflyrevisefundamentalnotionsfromcomplexitytheory.Weassumefa-miliaritywiththecomplexityclasses,,and-,andwiththenotionsofmany-one-reductions,Turingreductions,andhardnessandcompletenesswithrespecttothesereductions.
Thecomplexityoftheaboveproblemsforallframeworksandsemanticsweconsiderislocatedatthelowerendofthepolynomialhierarchy.Thisisa(pre-sumably)infinitehierarchyofcomplexityclassesaboveNPdefinedbyusingor-aclemachines,i.e.Turingmachinesthatareallowedtocallasubroutine—theoracle—decidingsomefixedprobleminconstanttime.Letbeaclassofde-cisionproblems.Then,denotestheclassofproblemsthatcanbesolvedonadeterministicoraclemachineinpolynomialtimewithanoraclethatdecidesaproblemin.Ingeneral,foranyclassdefinedbyresourcebounds,denotestheclassofproblemsdecidableonaTuringmachinewitharesourceboundgiven
byandanoracleforaproblemin.Basedonthesenotions,thesets
aredefinedasfollows:and
,
,
-
The“canonical”completeproblemsareSATfor=NPand-QBFfor
(),where-QBFistheproblemofdecidingwhetherthequantifiedbooleanformula
alternatingquantifiersstartingwith
istrue,foraformula.Theaboveproblemsremaincompletefortheirrespective
classeswhentheinnermostquantifierisandtheformulaisin3CNF,aswellaswhentheinnermostquantifierisandtheformulaisin3DNF[30].Thecomplementaryofa-QBFproblem,denotedbyco--QBF,iscompletefor.Allproblemsinthepolynomialhierarchycanbesolvedinpolynomialtimeiff.Further,alltheseproblemscanbesolvedbyworst-caseexponentialtimealgorithms.Thus,thepolynomialhierarchymightnotseemtoomeaning-ful.However,differentlevelsofthepolynomialhierarchydifferconsiderablyinpractice,e.g.methodsworkingformoderatelysizedinstancesofNP-completeproblemsdonotworkfor-completeproblems.
Thecomplexityoftheproblemsweareinterestedinhasbeenextensivelystud-iedforexistinglogicsfordefaultreasoningunderthestandard,stabilityseman-tics[3,15,23,19,29,2,10].Table1givesapartialsummaryoftheseresultsforthedifferentlogics.Wenoteherethatthesemanticsofcircumscriptionhasbeenoriginallyproposedwithrespecttoscepticalreasoningonly.Inthiscase,asshownin[1],reasoningincircumscription(restrictedtoHerbrandmodels)coin-cideswithscepticalreasoningintheoristunderthestabilitysemantics.Moreover,wecannaturallyextendcircumscriptionanddefineitscredulousreasoningviaaone-to-onecorrespondencewithcredulousreasoningintheoristunderthestabil-itysemantics(see[1]formoredetails).Hencethecomplexityresultforcredulousreasoningincircumscriptionisadirectconsequenceoftherespectiveresultfor
theorist.Thecomplexityresultsforreasoningincircumscriptionunderthead-missibilitysemantics,presentedlaterinthepaper,canbeunderstoodinasimilarway.
scepticalreasoning
NP-complete-complete-complete-complete-complete
Table1:Existingcomputationalcomplexityresultsforthestabilitysemantics
4GenericUpperBounds
Inthissectionwegiveanumberofgenericupperboundsforreasoningundertheadmissibilityandpreferabilitysemanticsthatareparametriconthecomplexityofthederivabilityproblemintheunderlyingmonotoniclogic.Thisallowsustoderiveupperboundsforawiderangeofconcretelogicsfordefaultreasoning.InthecaseofLP,theunderlyinglogicispropositionalHornlogic,hencethederivabilityproblemisP-complete(underlog-spacereductions)[24,p.176].Inthecaseoftheorist,circumscriptionandAEL,theunderlyinglogicisclassicalpropositionallogic,hencethederivabilityproblemis--complete.Finally,inthecaseofDL,theunderlyingmonotonicderivabilityisclassicalderivabilityextendedwithdomain-specificinferencerules.However,theseextrainferencerulesdonotincreasethecomplexityofreasoning.Indeed,itisknown(e.g.see[16,p.90])thatforanyDL-likepropositionalmonotonicrulesystem,checkingwhetherisNP-complete.Therefore,thefollowingpropositionfollowsimmediately.
Proposition1GivenaDLframework
Inordertodecidethecredulousandco-scepticalreasoningproblems,onecanapplythefollowingnon-deterministicalgorithm:Algorithm2
1.Guessanassumptionset,
2.verifythatitissanctionedbythesemantics,and
3.verifythattheformulaunderconsiderationisderivablefromthesetofas-sumptionsandthemonotonictheoryornotderivablefromit,respectively.Fromthisitfollowsthatcredulousreasoningandco-scepticalreasoningisinthecomplexityclass,providedreasoningintheunderlyinglogicisinandtheverificationthatanassumptionsetissanctionedbythesemanticscanbedonewithpolynomiallymanycallstoa-oracle.Forthestabilitysemantics,weneedindeedonlypolynomiallymany-oraclecallsinordertoverifythattheassumptionsetisnotself-attackingandthatitisclosedandattacksallassumptions.However,fortheadmissibilityandpreferabilitysemanticstheverificationstepdoesnotseemtobesoeasy,assuggestedbythefollowingtheorem.
Theorem3Forframeworkswithanunderlyingmonotoniclogicwithaderivabil-ityproblemin,theassumptionsetverificationproblemis
ininin
underthestabilitysemantics,
--
undertheadmissibilitysemantics,and
underthepreferabilitysemantics.
Proof:Thefirstclaimfollowsfromtheargumentabovethatpolynomiallymany-oraclecallsaresufficienttoverifythatanassumptionsetisstable.
Inordertoprovethesecondclaim,wegivethefollowingnondeterministic,
isnotpolynomial-timealgorithmthatusesa-oracleanddecideswhether
admissible:
1.Checkwhether
isclosed.Ifnot,succeed,otherwisecontinue.
2.Guessanassumptionset
.10
3.Verifythat4.Verifythat5.Verifythat
isclosed,usingattacks
-oraclecalls.
,using
-oraclecalls.
doesnotattack
,using
-oraclecalls.
isnotadmissible,i.e.,itdecidestheObviously,thisalgorithmsucceedsiff
complementoftheassumptionsetverificationproblem,thusprovingtheclaim.Inordertoprovethethirdclaim,foranyassumptionsetthatwewanttoverify,wegivethefollowingnondeterministic,polynomial-timealgorithmthatusesan-oracle:
-oraclecall(bythesecond1.Checkwhetherisadmissible,usingone
claim).Ifitisnot,succeed.Otherwisecontinue.
2.Guessanassumptionset
.
isadmissible,usingone3.Checkwhether
claim).Ifitis,succeed.Otherwisefail.
-oraclecall(bythesecond
isnotpreferred.Thismeansitde-Obviously,thisalgorithmsucceedsiff
cidesthecomplementoftheassumptionsetverificationproblem,thusprovingtheclaim.
1.Checkwhetherattacksitself,usingpolynomiallymany-oraclecalls.Ifitdoes,succeed.Otherwisecontinue.
2.Computea-oracle.
doesnotattack
,using
callsto
3.Checkwhetherattacks,usingpolynomiallymany-oraclecalls.Ifitdoes,succeed.Otherwisefail.
Itiseasytoseethatifthisalgorithmsucceedsthenisnotadmissible,asattacksbut,by(2),doesnotattackand,by(1),doesnotattackitself.Moreover,ifthealgorithmfailsthenisadmissible.Indeed,letbeanyattackagainst.If,then,bymonotonicityoftheunderlyinglogic,attacks,thuscontradictingthatthealgorithmfails.Therefore,.Let.By(2),attacks.Thus,attacks,and,by(1),isadmissible.
ThesecondclaimofthetheoremfollowsbyreconsideringthealgorithmusedintheproofofTheorem3forthethirdclaim,butusing-oraclecallsatsteps(1)and(3).
Notethatiftheframeworkisnotflat,thentheassumptionsetmightnotbeclosed.Therefore,evenif(3)succeeds,canstillbeadmissible,asitmayattackanassumptionthatisderivablefrom.
12
Proposition6Credulousreasoningundertheadmissibilitysemanticsisequiva-lenttocredulousreasoningunderthepreferabilitysemantics.
Thus,itfollowsdirectlythatcredulousreasoningundertheadmissibilityse-manticshasthesameupperboundascredulousreasoningunderthepreferabilitysemantics.Inparticular,fornormalframeworkswegetthesameupperboundforcredulousreasoningundertheadmissibilitysemanticsasforthestabilityseman-tics.
Inaddition,co-scepticalandscepticalreasoningundertheadmissibilityse-manticsisoftenmuchsimplerthansuggestedbytheupperboundsoftherespec-tiveassumptionsetverificationproblemcombinedwithalgorithm2.Forexample,inflatframeworks
simpleiffthereisnoadmissibleassumptionsetwheneverisinconsistentintheunderlyingmonotoniclogic,andotherwisethereexistsaminimal(withrespect
.tosetinclusion)admissibleset
Proposition7Forflatframeworksandforsimpleframeworkswithanunderlying
monotoniclogicwithaderivabilityproblemin,thescepticalreasoningproblemundertheadmissibilitysemanticsisin.
Alltheresultsinthissectioncombinedwithalgorithm2givethenextthe-orem,specifyingupperboundsforthereasoningproblemsforallthetypesofframeworksconsideredsofar.
Theorem8Upperboundsforthedifferentreasoningproblems,typesofframe-works,andsemanticsareasspecifiedinthefollowingtable:Frameworks
scept.
general
Admissibility
scept.
scept.
--
-
-
flat
-
Notethatnotalldeductivesystemsunderlyinganabstractframeworkareequippedwithanotionofinconsistency.Forexample,theinstanceoftheframeworkforLPisnot.Moreover,notethatthenotionofinconsistencyisaseparatenotionfromthatofcontrary.
13
Proof:Theresultsforthestabilitysemanticsfollowfromapplyingalgorithm2,
oracle(byTheorem3),andwithstep(2)ofthealgorithmsolvablebyacalltoa
step(3)solvablebyacalltoa-oracle.Thisgivesanupperboundof,whichcoincideswith,forboththecredulousandco-scepticalreasoningproblems.Theresultsfortheadmissibilitysemanticsinthefirstrowandforscepticalreasoningunderthepreferabilitysemanticsinthefirstrowfollowbythesameargument.
TheresultforcredulousreasoningunderthepreferabilitysemanticsinthefirstrowfollowsfromProposition6andthecorrespondingresultfortheadmissibilitysemantics.
Theresultsforadmissibilityandpreferabilitysemanticsinthesecondrowarejustifiedasfollows.Credulousreasoningunderadmissibilityandpreferabilitysemanticsaswellasco-scepticalreasoningunderthepreferabilitysemanticscanbeshowntobein,whichequals,byusingalgorithm2andapplyingPropositions6and5.Further,theupperboundforscepticalreasoningundertheadmissibilitysemanticsisthegeneralupperboundgiveninthefirstrow.
TheresultsforadmissibilityandpreferabilitysemanticsinthethirdrowfollowbyapplyingProposition7forscepticalreasoningunderadmissibilityand,fortheothercolumns,algorithm2andTheorem4.
Finally,theresultsforadmissibilityandpreferabilitysemanticsinthefourthrowarethegeneralresultsinthefirstrow,withtheexceptionoftheresultforscepticalreasoningundertheadmissibilitysemanticsgivenbyProposition7.
Proof:Circumscriptionisaspecialinstanceoftheorist.Thus,weonlyneedtoprovethetheoremfortheorist.
Ifthegiventheoristtheoryisinconsistentthenthecorrespondingframeworkadmitsnoadmissibleargument,asanyclosedassumptionsetattacksitself.Assumethatisconsistent.Then,weonlyneedtoprovethatattackseveryclosedassumptionsetwhichattacks.Now,ifisnosetthatattacks.If,thenattacksiffand,asisclosed,.Thus,necessarilyattacks.
,thenthereisinconsistent6
FlatFrameworks:LogicProgrammingandDe-faultReasoning
Asinthecaseoftheoristandcircumscription,inthecaseofLPandDLtheupperboundsspecifiedinTheorem8aretight.
SincetheconcreteframeworkforLPisflat,scepticalreasoningundertheadmissibilitysemanticsreducestoreasoningintheunderlyingmonotoniclogic,i.e.,derivabilityinpropositionalHorntheories,whichisP-complete.
Proposition13ScepticalreasoninginLPundertheadmissibilitysemanticsisP-complete.
FromTheorem8,againbecausetheLPframeworkisflat,credulousreason-,whichequalsingundertheadmissibilityandpreferabilitysemanticsisin
NP.NP-completenesscanbeobtainedasadirectcorollaryofanearlierresultbySacc`a[28],thattheexpressivepowerofDATALOGqueriesunderthe“pos-sibleM-stablesemantics”(correspondingtocredulousreasoningunderthead-missibilityandpreferabilitysemantics)coincideswithDB-NP,i.e.theclassofalldatabasesthatarerecognisableinNP.Fromthisresultthefollowingtheoremfollowsimmediately.
Theorem14CredulousreasoninginLPundertheadmissibilityandpreferabilitysemanticsisNP-complete.
AgainfromTheorem8,scepticalreasoninginLPunderthepreferabilityse-manticsisinco-,whichcoincideswith.-completenesscanbeob-tainedagainasadirectcorollaryoftheresultprovenagainbySacc`a[28],thatthe
expressivepowerofDATALOGqueriesunderthe“definiteM-stablesemantics”(correspondingtoscepticalpreferabilitysemantics)coincideswiththeclassDB-,i.e.theclassofalldatabasesthatarerecognisableinDB-.Fromthisresultthefollowingtheoremfollowsimmediately.
Theorem15ScepticalreasoninginLPunderthepreferabilitysemanticsiscomplete.
-
Therefore,forLP,credulousreasoningunderadmissibilityandpreferabilitysemanticshasthesamecomplexityasunderthestabilitysemantics(seeTable1),
16
whereasscepticalreasoningiseitheronelevellowerbuttrivial,undertheadmissi-bilitysemantics,oronelevelhigher,underthepreferabilitysemantics,thanunderthestabilitysemantics.
SincetheinstanceoftheframeworkforDLisflat,scepticalreasoningun-dertheadmissibilitysemanticsreducestoreasoningintheunderlyingmonotoniclogic,i.e.,derivabilityinpropositionalclassicallogic,whichisco-NP-complete.Proposition16ScepticalreasoninginDLundertheadmissibilitysemanticsisco-NP-complete.
ByProposition6,credulousreasoningunderthepreferabilitysemanticsco-incideswithcredulousreasoningundertheadmissibilitysemantics.FromTheo-rem8,credulousreasoningundertheadmissibilityandpreferabilitysemanticsisin,whichcoincideswith.-hardness,andtherefore-completeness,canbeprovenbyareductionfrom2-QBF.
Theorem17CredulousreasoninginDLundertheadmissibilityandpreferabilitysemanticsis-complete.
Proof:ByProposition6,itsufficestoprovethetheoremfortheadmissibilitysemantics.MembershipfollowsfromTheorem8.Toprovehardness,weuseastraightforwardreductionfrom2-QBFtothecredulousreasoningproblemundertheadmissibilitysemantics.
,withaAssumethequantifiedbooleanformula
formulain3DNFoverthepropositionalvariables.Wecon-structaDLtheorysuchthatthegivenquantifiedbooleanformulaistrueiffsomeadmissibleargumentfortheframeworkcorrespondingtocontains.Letconsistsofthedefaultrules
foreach,simulatingthechoiceofatruthvalueforeachpropositional
variablein.Obviously,canbeconstructedinlog-space.Moreover,itiseasytoseethatthegiven2-QBFistrueiffthereexistsanadmissibleextensionoftheframeworkcorrespondingtocontaining.
Theorem18ScepticalreasoninginDLunderthepreferabilitysemanticsiscomplete.
-
Proof:MembershipfollowsfromTheorem8.Toprovehardness,weuseare-ductionfrom3-QBFtotheco-scepticalreasoningproblemunderthepreferabilitysemantics.
Assumethequantifiedbooleanformula
withaformulain3CNFoverthepropositionalvariables,,
.WeconstructaDLtheorysuchthatistrueiffsomesentenceisnotcontainedinsomepreferredargumentfortheframeworkcorrespondingto.
Thelanguageofcontainsatoms,,andaswellasatoms,,intuitivelyholdingtrueiffatruthvalueforthevariables,,respectively,hasbeenchosen.consistsofthedefaultrules
foreach
andin,
,
,simulatingthechoiceofatruthvalueforeach
foreach
setcontains
,oranyof
toguaranteethatnoadmissibleassumptionand.
18
Obviously,canbeconstructedinlog-space.Moreover,weprovethatistrueiffthereisapreferredargumentnotcontaining.Inotherwords,the3-QBFcanbereducedtoco-scepticalreasoninginDLunderthepreferabilitysemantics.
Inthesequelwewillusethefollowingterminology.Ifisatruthassignmenttothe’s,wedenotebytheassumptionset
Similarly,ifset
isatruthassignmenttothe
’s,wedenoteby
theassumption
Firstofall,itisobviousthatnoadmissibleassumptionsetcancontainanyoftheassumptions,,(as,ifitdid,itwouldattackitself).Furthermore,itiseasytoseethatforanytruthassignmenttothe’s,thesetisanadmissi-bleset.Moreover,everypreferredassumptionsetmustcontainasetforsometruthassignmenttothe’s.Finally,ifisnotpreferred,thenthereexistsatruthassignmenttothe’ssuchthatispreferred.
Assumethatistrueunderaparticulartruthassignmenttothe’s.Obvi-ously,doesnotderive.Weshowthatthesetisapreferredassumptionset.
bytheset,forsometruthSupposethatitisnot,andthatwecanextend
assignmenttothe’s,thusobtaininganadmissibleset.Then,counterattackstheattack,i.e.belongstotheextensiongivenby.Asaconsequence,isnottrueunderthetruthassignment:contradiction.Conversely,assumethattheframeworkcorrespondingtoadmitsapre-ferredargumentthatdoesnotderive.Weprovethatistrue.Clearlythereexistssometruthassignmenttothe’ssuchthat.Sinceispreferredanditdoesnotcontain,noneofthesets,foreverypossibletruthassignmenttothe’s,isadmissible.Thismeansthatnoneofthesesetsofassumptionscancounterattacktheattackandderive.Therefore,istrue.
lowerbuttrivial,undertheadmissibilitysemantics,oronelevelhigher,underthepreferabilitysemantics,thanunderthestabilitysemantics.
NotethatsimilarresultstotheoneobtainedaboveforDLhavebeenrecentlyobtainedfordisjunctivelogicprogramming[11].
7GeneralFrameworks:AutoepistemicLogic
AELisneitherflat,simple,nornormal.ThismeansthatwecannotexpectanysimplificationswhenreasoninginAELframeworks.Asamatteroffact,theupperboundsforgeneralframeworks,whichapplyofcourse,arealsotightforAEL.ByProposition6,credulousreasoningunderthepreferabilitysemanticsco-incideswithcredulousreasoningundertheadmissibilitysemantics.FromTheo-rem8,sincethereasoningproblemintheunderlyingmonotoniclogicforAELisclassicalreasoninginpropositionallogic(coNP-complete),credulousreasoningundertheadmissibilityandpreferabilitysemanticsisin,whichcoincideswith.-hardness,andtherefore-completeness,canbeprovenbyareduc-tionfrom3-QBF.
Theorem19CredulousreasoninginAELundertheadmissibilityandpreferabil-itysemanticsis-complete.
Proof:ByProposition6,itsufficestoprovethetheoremfortheadmissibilitysemantics.MembershipfollowsfromTheorem8.Toprovehardness,weuseareductionfrom3-QBFtothecredulousreasoningproblemundertheadmissibilitysemantics.
Assumethefollowingquantifiedbooleanformula
withaformulain3CNFoverthepropositionalvariables,,.WeconstructanAELtheorysuchthatistrueiffsome
sentenceiscontainedinsomeadmissibleargumentfortheframeworkcorre-spondingto.
Thelanguageofcontainsatoms,,andaswellasatoms,intuitivelyholdingifatruthvalueforthevariables
hasbeenchosen,andanatomusedtopreventthatanytruthvalueforthe’scanbechosen.consistsofthesentences:
20
foreach,.
Obviously,canbeconstructedinlog-space.Nowweprovethattheframe-workcorrespondingtoadmitsanadmissibleextensioncontaining
iffistrue.Thismeansthatthegiven3-QBFcanbereducedtocredulousreason-ingundertheadmissibilitysemantics.
Assumethattheframeworkcorrespondingtoadmitsanadmissibleexten-sionderiving.Then,foreach,eitherorispartof,fortobederivedbyit.Further,mustbepartof,fortobeclosed,andthusadmissible.Finally,noneoftheassumptions,canbepartof,forotherwise,ifclosed,wouldattackitselfandthusbenon-admissible.Consideranyassumptionsetthatattacks.mustattackoneoftheas-sumptions,,or.However,ifattackedanyof,,thenwouldimmediatelycounter-attack.Therefore,fortobeanassumptionsetthatcanpossiblyrendernon-admissible,itmustmakethesamechoicesonthe’sas,andattack.Fortoattack,thenmustderive,byincluding,inadditiontotheassumptionsfromalreadychosenby,assumptionsfromtheset.Suchchoicescan-notbecounter-attackedbywithoutmakingitself-attacking.Therefore,sinceisadmissible,nosuchexists.Thismeansthat,forthegivenchoicesonthe’sin,nochoicesforthe’sexistthatmaketrue.Inotherwords,forthegivenchoiceofthein,andforallchoicesofthetruthvaluesforthe’s,thereexistsanassignmentoftruthvaluestothe’sthatmakestrue,whichimpliesthatisnecessarilytrue.
Conversely,assumethatthereisnoadmissibleextensionoftheframeworkcorrespondingtoderivingabove.Then,regardlessofthechoicesforthe’s,thereisalwaysanattackon,deriving,thatcannotbecounter-attackedwhilekeepingthecandidatesetofassumptionsnon-self-attacking.Then,bytheargumentspresentedabove,thegiven3-QBFformulacannotbetrue.
Theorem20ScepticalreasoninginAELundertheadmissibilitysemanticsiscomplete.
-
Proof:MembershipfollowsfromTheorem8.Toprovehardness,weuseare-ductionfrom3-QBFtotheco-scepticalreasoningproblemundertheadmissibilitysemantics.
WeusethereductionintheproofofthepreviousTheorem19,butextendthetheoryconstructedtheretothetheory.Anyadmissiblesetmustcontaintheassumptionsandinorderfortobeclosed.Furthermore,anyadmissibleextensionofmustcontainbecauseotherwiseitisattackedbywithouthavingacounter-attack.Fromthisfactandtheaboveobservationsitfollowsthathasanadmissibleextensioniffthegiven3-QBFformulaistrue.Giventhatifnoadmissibleextensionexistsallco-scepticalquerieswillbeanswerednegatively,theaboveisequivalenttothefactthatisnotascepticalconsequenceofiffistrue,i.e.,theconstructionisalog-spacereductionfrom3-QBFtoco-scepticalreasoningundertheadmissibilitysemantics.
consistsofthefollowingsentences:
(1)(2)(3)(4)(5)(6)(7)(8)
foreach
,,.Nowweclaimthatthereexistsapreferredextensionnotcontainingiffistrue.
First,onenotesthatanassumptionsetcontainingnon-conflictingassumptionsfromthesetisanadmissibleset.Letbeamaximalsuchset.Secondly,itisobviousthatcanbeexpanded(inanon-trivialway)onlybyaddingtheassumptionandassumptionsfromtheset.Letuscallthisexpandedset.Suchasetisonlyadmissibleifwemakechoicesforall’sbecauseotherwisecanbeattackedby(using)forwhichthereisnocounter-attackfrom.
Thirdly,thesetcannotbefurtherexpandedusingassumptionsfrombecausetheseassumptionsleadtoanimmediateself-attack.Fourthly,anassumptionsetcontainingassumptionsfromtogetherwithcanonlybeadmissibleifcannotbeattackedbyanyas-sumptionset.
Theonlywaytoconstructanattackagainst
in,whichisnotim-mediatelycounter-attackedby,wouldbetouseallassumptionsinandas-sumptionsfrom.Notethatsuchassumptionscannotbecounter-attackedby.Nowtheonlywaytoattackwouldbetomaketrue,andinordertodoso,onehastomaketrue.Assumingnowthatisadmissiblemeansthatforallpossiblechoicesforthe’s,isnotderivable,i.e.,thereisalwaysatruthassignmenttothe’sthatmakestrue.Thismeansthatcannotbeexpandedbyassumptionsfrom
togetherwith,ifunderthetruthassignmenttothe’scor-respondingtotheassumptionsin,foralltruthassignmentstothe’s,thereis
23
,
alwaysantruthassignmenttothe’sthatmakestrue.Inotherwords,ifthere
trueunder,istrue.existsapreferredassumptionsetthatdoesnotrender
Conversely,letusassumethatistrue.Letbeanassumptionsetcontainingassumptionsfromcorrespondingtoatruthassignmenttothe’sthatmakestrue.Thisassumptionsetcannotbeexpandedtobyassumptionsfromtogetherwith,becauseforanysuchexpansionthereexistsavalueassignmenttothe’swhichmakestrue,correspondingtoasetofchoicesfromwhichtogetherwithisanassumptionssetthatleadstogetherwithtothederivationofand,henceattacking.Forthisreason,thereexistsapreferredextensionnotcontainingbothandchoicesfrom,andhencethispreferred
.extensiondoesnotcontain
abstractframeworkfordefaultreasoningproposedin[1],foranumberofcon-creteinstancesoftheabstractframework,namelytheorist,circumscription,logicprogramming(LP),defaultlogic(DL)andautoepistemiclogic(AEL).Thesenewsemanticsarepresentedin[1]as“simpler”alternativestotheconventionalstabil-itysemanticsforallinstancesoftheframework(seeSection1foradiscussionofthisissue).
Table2summarisestheresultswehaveproven(fortheadmissibilityandpreferabilitysemantics)aswellasexistingresultsintheliterature(forthesta-bilitysemantics).Inthetable,“-c.”standsfor“-complete.”Wehaveproventheresultsbyappealingtopropertiesoftheframeworks,wheneverpossible.Inparticular,wehaveusedtheproperties(provenin[1])thatdefaultlogicandlogicprogrammingareflatframeworksandthattheoristandcircumscriptionarenormalframeworks.Inaddition,wehaveintroducedthenewpropertythatframeworksaresimple,andproventhattheoristandcircumscriptionsatisfysuchproperty.Autoepistemiclogicisageneralframeworkinthatitdoesnotsatisfyanyspecialpropertyamongsttheonesconsidered.
FrameworkAEL
flat
Theorist
Circumscription
Admissibility
scept.-c.
co-NP-c.P–c.
-c.-c.
scept.
-c.
-c.-c.
-c.-c.
Stability
scept.
-c.
-c.co-NP–c.-c.-c.
theframework,thusbecomingatrivialformofnon-monotonicreasoning.
ThereappearstobeaclashbetweentheseresultsandtheintuitionspelledoutinSection1,thatadmissibilityandpreferabilityargumentsareseeminglyeasiertocomputethanstableextensions.However,ourresultsarenotassurprisingastheymightatfirstappear.Sincetheadmissibilityandpreferabilitysemanticsdonotrestrictthenumberofextensions,onewouldexpectthatdefaultreasoningunderthesesemanticsisashardasunderthestabilitysemantics.Thehighercomplexityofthescepticalreasoningproblemunderthepreferabilitysemanticsisduetothefactthatinordertoverifythatanassumptionsetispreferred,oneneedstocheckthatnoneofitssupersetsisadmissible.
Ofcourse,ourresultsdonotcontradicttheexpectationthatinpracticecon-structingadmissibleargumentsisofteneasierthanconstructingstableextensions.
,withanysetofForexample,giventhepropositionallogicprogram
clausesnotdefiningtheatom,theemptysetforthequerythatcanbecon-structed“locally”,withoutaccessing.Moreover,ifislocallystrat-ifiedororder-consistent[1],isguaranteedtobeacredulousconsequenceoftheprogramunderthestabilitysemantics.Indeed,inallcaseswherethestabil-itysemanticscoincideswiththepreferabilitysemantics(e.g.forstratifiedandorder-consistentabstractframeworks)anysound(andcomplete)computationalmechanismfortheadmissibilitysemanticsissound(andcomplete)forthestabil-itysemantics.
The“locality”featureoftheadmissibilitysemanticsrendersitafeasiblealter-nativetothestabilitysemanticsinthefirst-ordercase,whenthepropositionalver-sionofthegivenabstractframeworkisinfinite.Forexample,giventhe(negation-free)logicprogram:,theemptysetofassumptionsisanadmis-sibleargumentforthequerythatcanbeconstructed“locally”,eventhoughthepropositionalversionofthecorrespondingabstractframeworkisinfinite.Thecomplexityresultsinthispapershowthatscepticalreasoningunderad-missibilityandpreferabilitysemanticsistrivialandhighlycomplex,respectively.However,thisdoesnotseemtomatterfortheenvisionedapplicationsofthisse-mantics,becausecredulousreasoningonlyisrequiredfortheseapplications[18].Forexample,inargumentationinpracticalreasoningingeneralandlegalreason-inginparticular,unilateralargumentsareputforwardsanddefendedagainstallcounterarguments,inacredulousmanner.Indeed,thesedomainsappeartobepar-ticularlywellsuitedforcredulousreasoningundertheadmissibilitysemantics.Ingeneral,theresultspresentedinthispaperindicatethatreasoningunderthenewsemanticsisharder.Onthepositiveside,theyindicatethatthenewsemantics
26
allowsustoencodemorecomplexreasoningpatternsthanwhenreasoningwiththestabilitysemantics.
Acknowledgments
ThefirstauthorhasbeenpartiallysupportedbytheDFGaspartofthegraduateschoolonHumanandMachineIntelligenceattheUniversityofFreiburgandthesecondauthorhasbeenpartiallysupportedbytheUniversityofCyprus.
References
[1]AndreiBondarenko,PhanMinhDung,RobertA.Kowalski,andFrancescaToni.Anabstract,argumentation-theoreticframeworkfordefaultreasoning.ArtificialIntelligence,93(1–2):63–101,1997.[2]MarcoCadoli,MaurizioLenzerini.TheComplexityofPropositionalClosedWorldReasoningandCircumscription.JournalofComputerandSystemSci-ences48(2):255–310,1994.[3]MarcoCadoliandMarcoSchaerf.Asurveyofcomplexityresultsfornon-monotoniclogics.TheJournalofLogicProgramming,17:127–160,1993.[4]YannisDimopoulos,BernhardNebelandFrancescaToni.PreferredArgu-mentsareHardertoComputethanStableExtensions,Proc.IJCAI’99,16thInternationalJointConferenceonArtificialIntelligence,pages36–41,T.Deaned.,MorganKaufmann,1999.[5]YannisDimopoulos,BernhardNebelandFrancescaToni.FindingAdmissibleandPreferredArgumentsCanBeVeryHard,Proc.KR’2000,7thInternationalConferenceonPrinciplesofKnowledgeRepresentationandReasoningpages53–61,T.Cohn,F.Giunchiglia,B.Selmaneds,MorganKaufmann,2000.[6]PhanMinhDung,RobertA.Kowalski,andFrancescaToni.SynthesisofProofProceduresforDefaultReasoning,Proc.LOPSTR’96,InternationalWorkshoponLogicProgramSynthesisandTransformation,pages313-324J.Gallaghered.,LNCS1207,SpringerVerlag,1996.
27
[7]PhanMinhDung,RobertA.Kowalski,andFrancescaToni.Argumentation-theoreticproofproceduresfordefaultreasoning.Technicalreport,ImperialCollege,London,UK,1998.[8]PhanMinhDung.Negationashypothesis:anabductivefoundationforlogicprogramming.InK.Furukawa,editor,Proceedingsofthe8thInternationalConferenceonLogicProgramming,pages3–17,Paris,France,1991.MITPress.[9]ThomasEiterandGeorgGottlob.Reasoningwithparsimoniousandmoder-atelygroundedexpansions.FundamentaInformaticae17(1,2):31–54,1992.[10]ThomasEiterandGeorgGottlob.PropositionalCircumscriptionandEx-tendedClosed-WorldReasoningare-Complete.TheoreticalComputerSci-ence114(2):231–245,1993.
[11]ThomasEiter,NicolaLeone,andDomenicoSacc`a.Expressivepowerandcomplexityofpartialmodelsfordisjunctivedeductivedatabases.TheoreticalComputerScience,206:181–218,1998.[12]KaveEshghiandRobertA.Kowalski.Abductioncomparedwithnegationasfailure.InG.LeviandM.Martelli,editors,Proceedingsofthe6thInternationalConferenceonLogicProgramming,pages234–254,Lisbon,Portugal,1989.MITPress.[13]MichaelR.GareyandDavidS.Johnson.ComputersandIntractability—AGuidetotheTheoryofNP-Completeness.Freeman,SanFrancisco,CA,1979.[14]MichaelGelfondandVladimirLifschitz.Thestablemodelsemanticsforlogicprogramming.InK.BowenandR.A.Kowalski,editors,Proceedingsofthe5thInternationalConferenceonLogicProgramming,pages1070–1080,Seattle,WA,1988.MITPress.[15]GeorgGottlob.Complexityresultsfornonmonotoniclogics.JournalforLogicandComputation,2(3):397–425,1992.[16]GeorgGottlob.Thecomplexityofdefaultreasoningunderthestationaryfixedpointsemantics.InformationandComputation,121:81–92,1995.
28
[17]AntonisC.Kakas,RobertA.KowalskiandFrancescaToni.Theroleofabductioninlogicprogramming.HandbookofLogicinArtificialIntelligenceandLogicProgramming,5:235–324,D.M.Gabbay,C.J.HoggerandJ.A.Robinsoneds.,OxfordUniversityPress,1998.[18]RobertA.KowalskiandFrancescaToni.Abstractargumentation.JournalofArtificialIntelligenceandLaw,4(3–4):275–296,1996.[19]VictorW.MarekandMiroslawTruszczynski.Nonmonotoniclogic:context-dependentreasoning.Springer-Verlag,Berlin,Heidelberg,NewYork,1993.[20]JohnMcCarthy.Circumscription—aformofnon-monotonicreasoning.Ar-tificialIntelligence,13(1–2):27–39,1980.[21]DrewMcDermott.NonmonotoniclogicII:Nonmonotonicmodaltheories.JournaloftheAssociationforComputingMachinery,29(1):33–57,1982.[22]RobertC.Moore.Semanticalconsiderationsonnonmonotoniclogic.Artifi-cialIntelligence,25:75–94,1985.[23]IlkkaNiemel¨a.Towardsautomaticautoepistemicreasoning.InLogicsinAI,volume478ofLectureNotesinArtificialIntelligence.Springer-Verlag,Berlin,Heidelberg,NewYork,1990.[24]ChristosH.Papadimitriou.ComputationalComplexity.Addison-Wesley,Reading,MA,1994.[25]DavidPoole.Alogicalframeworkfordefaultreasoning.ArtificialIntelli-gence,36:27–47,1988.[26]RaymondReiter.Alogicfordefaultreasoning.ArtificialIntelligence,13(1):81–132,April1980.[27]DomenicoSacc`aandCarloZaniolo.Stablemodelsandnon-determinisminlogicprogramswithnegation.InProceedingsofthe9thACMSIGACT-SIGMOD-SIGARTSymposiumonPrinciplesofDatabase-Systems(PODS-90),pages205–217,1990.[28]DomenicoSacc`a.Theexpressivepowerofstablemodelsforboundandun-boundDATALOGqueries.JournalofComputerandSystemSciences,54:441–464,1997.
29
[29]J.Stillman.Thecomplexityofpropositionaldefaultlogics.InProceed-ingsofthe10thNationalConferenceoftheAmericanAssociationforArtificialIntelligence(AAAI-92),pages794–799,SanJose,CA,July1992.MITPress.[30]L.StockmeyerandA.Meyer.WordProblemsRequiringExponentialTime:PreliminaryReport.InProceedingsofthe5thACMSymposiumontheTheoryofComputing,(STOC1973),pages1–9,1973.
30
因篇幅问题不能全部显示，请点此查看更多更全内容