Akrewrite规则

AbductiveLogicProgrammingbyNongroundRewriteSystemsFangzhenLinDepartmentofComputerScienceHongKongUniversityofScienceandTechnologyClearWaterBay,Kowloon,HongKongJia-HuaiYouDepartmentofComputingScienceUniversityofAlbertaEdmonton,Alberta,CanadaAbstractLogicprogrammingwithnegationoffersacompellingap-proachtoabductivereasoning.
Thispapershowsasimpleviewofabductioninthiscontextforthecompletionseman-tics,underwhichtheproblemofabductionbecomesoneofsolvingquantiedequationsanddisequations.
Bythiswayoftreatingabduction,theproblemswithnongroundnegativequeriesinthepreviousapproachesnolongerexist.
Weshowthesoundnessandcompletenessresultsforourapproach.
IntroductionLogicprogrammingwithnegationhasbeenconsideredanattractiveapproachtoabduction(Kakas,Kowalski,&Toni1995).
Thegoalistoshowthatanobservation,intermsofaquery,canbeexplainedbyareasoningprocesssupportedwithhypotheses,calledabducibles,whilesatisfyingpostedconstraints.
Anumberofapproachestoabductivelogicprogramminghavebeenproposed.
Oneapproachisbasedonthe(par-tial)stablemodelsemantics(e.
g.
,(Eshghi&Kowalski1989;Kakas,Michael,&Mourlas2000;Lin&You2002)).
Theseproofproceduresaredesignedessentiallyforgroundpro-grams.
Anotherfamilyofproceduresareproposedfornongroundprogramsunderthecompletionsemantics(Con-sole,Theseider,&Porasso1991;Fung&Kowalski1997;Endrissetal.
2004),wheretheuseoftheIFFdenitionsasrewriteruleshasconsiderablysimpliedtheproofprocess,andmadeabductivereasoningmoreintuitiveandtranspar-ent.
ThisisincontrastwiththeapproachbasedonnestedprooftreescalledtheSLDNFAprocedure(Denecker&DeSchreye1998).
Iffdenitionsmaycontainexistentialvariables.
Whennegated,theybecomeuniversallyquantied.
Sincelogicprogrammingtraditionallycanonlyprocessquerieswithex-istentialvariables,processingquerieswithuniversalvari-ableshasbeensaidtobeunsafe.
Inthepast,allproofpro-ceduresaredesignedtosatisfysomesafetyconditions.
Agoalissaidtoounderifallofitssubgoalsarenon-groundnegativeliterals.
Topreventagoalfromounder-ing,thebest-knownsyntacticconditionistheso-calledal-lowednesscondition.
Aniffdenitionp(X)D1∨.
.
.
∨DmCopyrightc2008,AssociationfortheAdvancementofArticialIntelligence(www.
aaai.
org).
Allrightsreserved.
isallowedifeveryvariableotherthanXoccurringinaDioccursinapositivenonequalityatominthesameDi;simi-larlyforqueries,constraints,andsetsofiffdenitions.
Allowednessreinforcesaprogrammingstyleinwhichev-eryvariablethatmaypotentiallybecomeuniversallyquan-tiedmustbe"grounded"byadomaindenition,sothatounderingcanbeavoidedbyinstantiatingthevariablesinanegativesubgoalbeforeitsproofisattempted.
Forsmalldomains,suchanapproachisne.
Butforlargeorin-nitedomains,itmakesprogrammingtediousandreasoninginefcient,asinsuchaprocedureamechanismofenumer-atingdomainelementsistightlycoupledwiththeprocessofprovingnegativesubgoals.
Forexample,ifwehaveafactmember(X,[X|R])inourprogram,thecompleteddeni-tionofmemberisnotallowed:member(X,Y)Y=[X|R]∨.
.
.
sincevariableRdoesn'tappearinapositivenonequalityatom.
OnecanmakethedenitionallowedbyarecursivedenitionoflistandrestrictingRtothatdomain.
Onewouldexpectthat,designedspecicallyforaclassofwell-behavedprograms,namelyallowedprograms,aproofprocedurewouldbesimpler.
Itturnsoutallofthepreviousproofproceduresareformulatedinsomecomplexways.
Thispapershowsthatamuchsimplerviewofabductionispossible,evenfortheclassofallprogramsandgoals.
Weshowthattheproblemofabductioncanbepartitionedintotwosubproblems,therstofwhichistotransformagoaltoaformulacontainingquantiedequalitiesanddisequalities,whichcanthenbesolvedseparately.
Sincevariablequanti-cationisrepresentedexplicitlyaccordingtothesemantics,theprobleminthepastwithnongroundqueriessimplybe-comesanon-issueinourapproach.
Thisapproachissoundwhere|=isinterpretedin2-valuedlogic.
Forcompleteness,|=hastobeweakenedto3-valuedlogic.
DenitionsWeconsiderarst-orderlanguageL.
Variablesbeginwithacapitalletter,andpredicate/function/constantsymbolsbeginwithalowercaseletter.
ForanysyntacticentityΦ,V(Φ)denotesthesetofthevariablesappearingfreeinΦ.
AconjunctionA1∧.
.
.
∧Akmaybewrittenas[A1,.
.
.
,Ak].
WewriteΦtomeanthatallthevariablesappearingfreeinformulaΦareuniversallyquantied,similarlyforΦ.
WeusethenotationΘtode-noteavectorofvariablequantication,suchasXYforinstance.
WeassumetheClark'sequalitytheory(Clark1978),writ-tenCETbelow,whichessentiallysaysthatallsyntacti-callydistinctgroundtermsarenotequal,andthatfunc-tionsareone-to-one:X,Yf(X)=g(Y)foranytwodis-tinctfunctionsymbols(includingconstants)fandg,andX,Yf(X)=f(Y)→X=Y.
Wealsoassumethatthelanguageincludesallsymbolsinthegivenprogram.
Thusifaandboccurintheprogramastwoconstants,thenCETwillincludetheaxioma=b.
AnabductiveprogramisatripleT,IC,Ab,where1.
Tisanitesetofiffdenitionsoftheformp(X1,.
.
.
,Xn)D1∨.
.
.
∨Dm(1)wherepisann-arydenedpredicatesymbol(denotedp/n),X1,.
.
.
,Xnaredistinctvariables,andDiaconjunctionofliterals.
ThevariablesX1,.
.
.
,Xnareimplicitlyuniversallyquantiedwiththescopebeingtheentiredenition,andanyothervariableoccurringinanyDiisexistentiallyquantiedwiththescopebeingDi.
Whenm=0,therighthandsideof(1)isfalse.
Iffdenitionsarethecompleteddenitionsofthepredi-catesinanormalprogramP,denotedcomp(P),accordingto(Clark1978).
Forconvenience,andalsoforintuition,inexpositionwemayjustgiveanormalprograminsteadofitscompletion.
AnormalprogramisanitesetofnormalrulesoftheformA←B1,.
.
.
,Bj,notC1,.
.
.
,notCk.
,wherej,k≥0,A,BiandCiare(nonequality)atoms.
Thelogicalformulaforthecompletionofp/nisXp(X)mi=1Yi[(X=si)∧Φi)](2)whereXisanabbreviationofX1,.
.
.
,Xn,andeachdis-junctcorrespondstoaDiintheform(1),where,forthecorrespondingnormalrulewithp/ninthehead,X=siistheconjunctionofequationsrepresentinguniability,Yide-notesthevariablesotherthanXthatappearinthedisjunct,andΦiistherulebodywithnotreplacedby.
Thenegationofanequation,(s=t),iscalledadise-quationandwillbewrittenass=t.
Weuseequationandequalityinterchangeably.
Wewrite(t=s)byt=s.
2.
ICisaconsistentnitesetofconstraintsoftheform⊥←A1,.
.
.
,Ak,B1,.
.
.
,BmwhereAiandBiareatoms.
Allvariablesinaconstraintareuniversallyquantied.
3.
Abisanitesetofpredicatesymbols,calledabducibles,whicharedifferentfrom=andanydenedpredicatesym-bol.
Aquery,alsocalledagoal,isaconjunctionofliterals.
Allvariablesappearinginagoalarefree.
Duringderiva-tion,aderivedgoalmaybeacomplexformulainvolving∧,∨and,andsomevariablesmaybecomeuniversallyquantied.
Thus,agoalisgenerallycalledagoalformula,whichformallyisaformulaoftheformΘΦ,whereΦisaquantier-freeformulawithnegationappearingonlyinfrontofanatom.
GivenanabducibleprogramT,IC,AbandaqueryG,theinitialqueryisthegoalformulaX.
G∧ΦIC,whereΦICistheconjunctionoftheconstraintsinICbyconvertingaconstraintoftheform⊥←A1,.
.
.
,Ak,B1,.
.
.
,Bmintothedisjunction[A1∨.
.
.
∨Ak∨B1∨.
.
.
∨Bm].
XisthetupleofvariablesinIC.
WeassumeherethatGandICdonothavecommonvariables-thiscanbeachievedbyvariablerenamingifnecessary.
Thustheini-tialqueryislogicallyequivalenttoG∧XΦIC.
Wemoveallquantierstotheoutsideduringrewriting.
Inthefollowing,weshallabusethelanguageanduseICtostandforitscorrespondingformulaΦICaswell.
Thuswe'llwritetheinitialqueryasX.
G∧IC.
AnanswertoaqueryGisapair(,σ),whereisanitesetofgroundabducibleatoms,andσisasubstitutionofgroundtermsforvariablesinV(G),suchthatT∪comp()∪CET|=Gσ∧XIC.
(3)Wemaysimplycallσananswerwhentherearenoab-duciblesinvolved.
Thesymbol|=referstothe2-valueden-tailmentrelationifnotsaidotherwise.
OurobjectiveinthispaperistoproposeasetofrulestorewriteaninitialqueryintoaformulaoftheformΘ(E∨Φ),andthenextractanswersfromEwhenEcontainsonly=andabducibles.
GoalRewritingunderCompletionSemanticsAgoalrewritesystemisatransformationsystemthatcon-sistsofiffdenitionsforunfolding,augmentedbysomesimplerulesforequivalence-preservingtransformations.
SimplicationrulesWeusesymbolsTandFforbooleanconstantstrueandfalse,respectively.
LetΘΠbeagoalformula.
Πcanberewrittenaccordingtothefollowingrules(andtheirsym-metriccases).
SR1.
F∨Φ→ΦSR2.
F∧Φ→FSR3.
T∧Φ→ΦSR4.
T∨Φ→TSR5.
(Φ1∨Φ2)∧Φ3→(Φ1∧Φ3)∨(Φ2∧Φ3)WeassumethatTwillberewrittentoFandFtoT,automatically.
RewriterulesforunicationLetEbeaconjunctionofequalities.
LetδbethemguofEwhenEisuniable.
Wewillwriteδasasetofequations.
WedeneδE=Tifδ=,andδE=δotherwise.
Unicationrules:(1)E→FifEisnotuniable(2)E→δEifEisuniable(3)X=t∧Φ→X=t∧Φ{X/t},whereXdoesnotoccurintandΦ{X/t}istheresultofreplacingXinΦbyt.
(4)X=t∨Φ→X=t∨Φ{X/t}Theunicationrulesshouldbeappliedwheneverpossibletopropagatetheunierandtopreventnon-uniablepatternsfrombeingpursued.
UnfoldingUnfoldingapositiveliteralisclear.
UnfoldinganegativeliteralraisesthequestionofquanticationforvariablesinDi'sotherthanX1,.
.
.
,Xn.
Givenacompleteddenitionintheform(2),anegativeliteralp(t)willbeunfoldedaccordingtothefollowingequivalences.
p(t)mi=1Yi[t=si∨Φi](i)mi=1Yi[t=si∨[t=si∧Φi]](ii)mi=1Yi[t=si]∨ZiRi[(t=si∧Φi){Yi/Zi}](iii)whereYi=V(si),whicharerenamedtoZiintheseconddisjunct(bysubstitution{Yi/Zi})andbecomeexistentiallyquantied,andRi=Yi\Yiaretheremainingvariables.
HerewehaveassumedthatV(t)∩Yi=foreachi.
ThiscanalwaysbeachievedbyrenamingvariablesinYiwhennecessary.
Forinstance,givenp(V)X,Y,Z(V=s(X,Y)∧q(Y,f(Z))),forp(f(X)),theformula(i)aboveisX1,X2,X3(f(X)=s(X1,X2)∨q(X2,f(X3))),andtheformula(iii)isX1,X2(f(X)=s(X1,X2))∨Y1,Y2X3(f(X)=s(Y1,Y2)∧q(Y2,f(X3))).
Thesignicanceoftheformula(iii)isthefollowing.
Asmentionedearlier,thepurposeofrewritingistogenerateagoalformulaoftheformΘ(E∨Φ)suchthatEmentionsonly=andabduciblesandthentoextractanswersfromΘE.
Ingeneral,Θ(E∨Φ)≡ΘE∨ΘΦ.
However,insomesitu-ations,e.
g.
,whenEandΦdonotshareuniversalvariables,thetwoarelogicallyequivalent.
Inthiscase,ΘEcanbeevaluatedindependently,soisΘΦ.
Theformula(iii)sayssomeuniversalvariablesresultedfromaniffdenitioncanbeconvertedtoexistentialones,thusreducingthechancesofshareduniversalvariables.
Thiswillsimplifytheprocessofanswerextraction(cf.
thenextsection).
Wenowprovethattheequivalence(iii)indeedholdsun-derthecompletionsemantics.
Lemma1(Correctnessofunfolding)GivenaprogramP,apredicatep,andacompleteddeni-tionintheform(2),letp(t)beanatomsuchthatV(t)∩Yi=foreachi.
Then,comp(P)∪CETentails(a)p(t)mi=1Yi[(t=si)∧Φi](b)p(t)theformulain(iii)above.
Proof.
Thecorrectnessofpart(a)isclear.
Let'sprovepart(b).
Itisclearthatundercomp(P),p(t)isequivalenttotheformula(ii)above,whichisequivalenttomi=1YiRi[t=si∨[t=si∧Φi]],thusequivalenttomi=1Yi[t=si∨Ri[t=si∧Φi]]asthevariablesinRidonotoccurintandsi.
Itiseasytoseethatthisformulaentailstheformulain(iii)above.
WeshowthattheotherwayaroundisalsotrueunderCET.
Toshowthis,weprovethatunderCET,foreachi,ZiRi[(t=si∧Φi){Yi/Zi}](4)entailsYi[t=si∨Ri[t=si∧Φi]].
(5)Toshowthis,supposeRi[(t=si∧Φi){Yi/Zi}],(6)t=si.
(7)From(6),weget(t=si){Yi/Zi},thust=(si{Yi/Zi})sinceYidoesnotoccurint.
Soby(7)wehavesi=(si{Yi/Zi}),thusZi=YibyCET.
Fromthisand(6),wegetRi[(t=si∧Φi)].
ThuswehaveshownthatCET|=(6)→[t=si∨Ri[t=si∧Φi]].
Soby-introduction,wehaveCET|=(6)→(5),andby-introduction,wehaveCET|=(4)→(5).
2Withthislemma,wecannowdeneunfoldingrules.
UnfoldingLetΠ=ΘΦbeagoalformula.
1.
Ifp(t)occursinΦpositively(i.
e.
notunderoperator),thenrewriteΠintothefollowinggoalformulaΘY1···YmΦ,whereΦistheresultofreplacingthisoccurrenceofp(t)bymi=1(t=si)∧Φi.
HereweassumethatthefollowingsetsofvariablesV(Φ),Y1,Ymarepair-wisedisjoint.
ThiscanbeachievedbyrenamingvariablesinYiifnecessary.
2.
Ifp(t)occursinΦ,thenrewriteΠintothefollowinggoalformulaΘY1Z1R1···YmZmRmΦ,whereΦistheresultofreplacingthisoccurrenceofp(t)bymi=1t=si∨(t=si∧Φi){Yi/Zi},whereΦi,thecomplementofΦi,isA1Ak∨B1BnwhenΦiisA1Ak∧B1Bn.
AgainweassumethatthefollowingsetsofvariablesV(Φ),Y1,Z1,R1,Ym,Zm,Rmarepair-wisedisjoint.
Againthiscanbeachievedbyvari-ablerenamingifnecessary.
Asanexample,supposewehavep(V)V=s(X,Y)∧q(Y,f(Z))q(Y,Z)Y=L∧Z=L∧r(L,K).
ForthegoalX(p(X)∧q(X,Y)),Ifweunfoldp(X)init,wegetX,X1,X2,X3[X=s(X1,X2)∧q(X2,f(X3))∧q(X,Y)].
Ifweunfoldq(X,Y)init,wegetXX1X2X3[p(X)∧((X=X1∨Y=X1)∨(X=X2∧Y=X2∧r(X2,X3)))].
RewriteSystemandAnswerExtractionInthefollowing,givenagoalformulaΠ,wewriteΠΠifΠcanbewrittenintoΠbyoneapplicationoftherulesintroducedsofar,anddenotebythetransitiveclosureof.
Proposition1IfΠΠ,thencomp(P)∪CET|=X(ΠΠ)whereXisthetupleoffreevariablesinΠ.
Proof.
Weonlyneedtoprovethisforthesinglestepcase.
Thecasesforsimplicationandunicationrulesareobvi-ous.
Fortheunfoldingrules,theyfollowfromLemma1bynotingthatinrst-orderlogic,ifXandYaredifferentvari-ables,Xdoesnotoccurin,andYdoesnotoccurinφ,then(Q1XQ2Yφ)Q1XQ2Y(φ),whereQiiseitheror,andiseither∧or∨.
2ThisshowsthatourrewritesystemissoundunderthecompletionsemanticsandClark'sequalitytheory.
Aswementioned,givenaninitialqueryX.
G∧IC,ourobjectiveistorewriteitintoaformulaoftheformΘ(E∨Φ)suchthatEmentionsonly=andabducibles,andthenextractanswersfromE.
Wenowmakethisprocessprecise.
Inthefollowing,givenΘ(E∨Φ),wecallΘEapre-answerformulaifEisquantier-freeandmentionsonly=andabducibles.
Inaddition,ifEdoesnotmentionab-ducibles,thenwecallΘEananswerformula.
NotethatanabducibleinEmayappearpositivelyornegatively,andΘEmaycontainuniversalorexistentialvariables.
GivenΘE,andanitesetDofgroundatomsaboutabduciblepredi-catesinE,weabducethepre-answerformulaΘEtotheanswerformulaΘEDbythefollowingtransformation:foreveryabducibleabthatappearsinEandthesubsetofDaboutabdenedasDab={ab(si)∈D},anyoccurrenceofab(t)inEisreplacedbyit=si,andab(t)byit=si.
TheintuitionhereisthatifDdenesabduciblesinE,thenΘEandΘEDareequivalent.
Inotherwords,ΘEandΘEDareequivalentundercomp(D).
AnswerExtractionLetT,IC,Abbeanabductivepro-gramandGagoal.
AssumethattheinitialqueryX.
G∧IChasbeenrewrittentoΘ(E∨Φ),whereΘEisapre-answerformula.
Letbeanitesetofgroundabducibleatoms,andσ={X/t|X∈V(G)}asubstitutionforvariablesinV(G).
Wesaythat(,σ)isextractedasananswertoG,basedonE,ifCET|=ΘEσ.
IfagoalformulaΘEitselfisalsoapre-answerformulaandnoanswercanbeextractedfromit,thentheproofoftheinitialgoalfailed.
Itisconvenienttomakethisexplicit.
Ruleofanswerextractionfailure:LetΘEbeagoalfor-mularewrittenfromsomeinitialquerysuchthatΘEisalsoapre-answerformula.
ΘE→FifnoanswercanbeextractedfromΘEWenotethatProposition1canbeextendedwiththeaddi-tionofthisnewrule.
Weshallshowthatourrewritesystemwithanswersex-tractedthiswayissoundandcomplete.
Beforewedothis,weshowsomeexamples.
ExamplesExample1LetT,,beanabductiveprogram,whereTis{p(X)r(X,Y);r(X,Y)X=a∧Y=b}.
Clearly,T∪CET|=p(t),foranytinthelanguage,whichaswesaidinSection2,includesatleastaandb.
Wecanshowthisusingourrewritesystemasfollows:p(V)Yr(V,Y)Y(V=a∨Y=b)Wegetthreepre-answerformulasfromthis:Y(V=a),Y(Y=b),andY(V=a∨Y=b).
Fromthesecondone,weextracttheanswer(,{V/t})foranyt.
Ontheotherhand,weexpectp(V)tobeprovedfalse.
p(V)Yr(V,Y)Y(V=a∧Y=b)FThisisbecauseCET|=Y(Y=b)asourlanguagecon-tainsbothaandb.
Thisshowsthereisnotsuchthatp(t)followsfromT∪CET.
2Thisisasimpleprogram.
Formoreinvolvedones,therewouldbemanyvariablesandquantiers,anditmaybecomedifculttotrackwhethertheyareuniversalonesorexisten-tialones,andtheirnestedorder.
Toalleviatethis,wepro-poseanexplicitrepresentationofquanticationforgoalfor-mulasusinganannotatednotation.
LetΠ=Q1ξ1.
.
.
QkξkΦbeagoal,whereΦisaformulawithkvariablesξ1,.
.
.
,ξk,andeachQiiseitheror.
Intheconstructionofaproofbyrewriting,wewillwriteΠasΦ,whereΦisobtainedfromΦbyreplacingeachvariableξibyXQi.
Forexample,XY[f(X,X)=f(a,Y)∧p(Y)]canberepresentedbyf(X1,X1)=f(a,X2)∧p(X2).
Inthefollowing,weshallusethesetwonotations,regulargoalformulasandtheirannotatedversions,interchangeably.
Inourdenitionofunfolding,wepushallvariablestotheoutside,andtodothis,wehavetorenamevariablestoavoidnameconicts.
Wenowuseanexampletoshowthatthisisnecessary.
Otherwise,onewouldhavetodesignmoreinvolveddistributionrules.
Example2Considerthefollowingprogramp(X)←r(X),q(Y).
q(X)←q(X).
q(X)←s(X,Y).
r(a).
s(a,b).
anditscompletionp(X)r(X)∧Yq(Y),q(X)q(X)∨Ys(X,Y),r(X)X=a,s(X,Y)X=a∧Y=b.
Itiseasytoseethatp(a)a=a∧q(X1)∨(a=a∧X1=a∧X2=b)SinceCETentailstheanswerformulaX1,X2(a=a∧X1=a∧X2=b),thequeryisansweredpositively.
How-ever,ifwedonotmovethequantierstotheoutside,wewouldget:p(a)r(a)∧Yq(Y)a=a∧Y(q(Y)∨Zs(Y,Z))a=a∧Y(q(Y)∨Z(Y=a∧Z=b)).
Toextractanswersfromtheabove,wewouldneedtohaverulesthatcandistributequanticationstoget,forexample,theanswerformulaa=a∧Y,Z(Y=a∧Z=b).
2Wementionedearlierthatfornegativeliterals,theuseoftheformulain(iii),insteadoftheformulain(i)or(ii),cansimplifytheprocessofanswerextraction.
Wenowillustratethisbythefollowingexample.
Example3ConsiderTthatconsistsofeven(V)[V=0]∨[V=s(s(Y)),even(Y)]Weexpectqueryeven(X)tobeprovedwithXboundtos(0),s3(0),andsoon.
even(X)X=0∧[X=s(s(Y1))∨(X=s(s(Y2))∧even(Y2))][X=0,X=s(s(Y1))]∨[X=0,X=s(s(Y2)),even(Y2)][X=0,X=s(s(Y1))]∨[X=0,X=s(s(Y2)),Y2=0,Y2=s(s(Z3))]∨[X=0,X=s(s(Y2)),Y2=0,Y2=s(s(Z3)),even(Z3)]Inthelastgoalformula,ananswerX=s(0)isextractedfromtherstdisjunct.
Bydenition,thiscanbeexpressedformallyasCET|=Y[X=0,X=s(s(Y))]{X/s(0)}Similarly,X=s(s(s(0)))isextractedfromtheseconddis-junctabove.
Wementionedthatthelanguagecanhavesymbolsnotintheoriginalprogram.
Supposenowthereisonemorecon-stantainthelanguage.
Thenwecanextractadditionalan-swers,X=aandX=s(a),fromtherstdisjunctabove,andX=s(s(a))andX=s(s(s(a)))fromthesecond.
Indeed,itiseasytoseethatT∪CET|=even(t),fort=a,s(a),s(s(a)),etc.
Thusthefunction"s"(successor)doesnothaveitsintendedmeaningwhenappliedtotermsformedbythenewconstanta.
Thiscanbexedbyaddingeven(a)(oreven(s(a))ifonewantsatorepresentanoddnumber)totheprogram.
Nowsupposeweusetheformulain(i)torewriteanega-tiveliteralinthegoalformula,wewillgeteven(X)Y[X=0,X=s(s(Y))]∨[X=0,even(Y)]YZ[X=0,X=s(s(Y))]∨[X=0,Y=0,Y=s(s(Z))]∨[X=0,Y=0,even(Z)]Forexample,theanswerX=s(s(s(0)))cannotbeex-tractedfromtheseconddisjunctalone,astheanswerfor-mulaYZ[s(s(s(0)=0,Y=0,Y=s(s(Z))]isnoten-tailedbyCET.
Butthisanswercanbeextractedfromthersttwodisjunctstogether,namely,CET|=YZ[s(s(s(0)))=0,s(s(s(0)))=s(s(Y))]∨[s(s(s(0)))=0,Y=0,Y=s(s(Z))]Inthisexample,inordernottomissanyanswer,allan-swerformulastogethermustparticipateinanswerextrac-tion.
Clearly,thisisamuchharderjobthanextractingan-swersfromeachdisjunctindependently.
2Wenowshowsomeexamplesthathaveabducibles.
Example4Consideranabductiveprogramandagoal.
T={q(X)ab(X);p(X,Y)X=f(V)∧Y=W}IC={[ab(X)∨p(X,Y)]},Ab={ab},andthegoalisq(I).
[q(I),[ab(X1)∨p(X1,X2)][ab(I),[ab(X1)∨p(X1,X2)][ab(I),[ab(X1)∨[X1=f(X3),X2=X4]]]Thisisapre-answerformula.
SincetheconjunctX2=X4isentailedbyCETindependently,itcanbedropped.
De-notetheresultingformulabyE.
Let={ab(f(a))}.
Then,E=[I=f(a),[X1=f(a)∨X1=f(X3)]]Clearly,(,{I/f(a)})isananswertothegoal.
But({ab(a)},{I/a})isnot,sinceICisnotsatised.
2Example5Considerthefaulty-lampexampleof(Fung&Kowalski1997).
Forsimplicity,letusconsideronlyonewayforthelamptobefaulty.
SupposetheabductiveprogramisT,,{powerfailure,empty},whereTisfaultylamppowerfailure(X)∧backup(X)backup(X)battery(X,Y)∧empty(Y)battery(X,Y)X=b∧Y=cTheabbreviationsusedbelowshouldbeclear.
fl[pf(X1),backup(X1)][pf(X1),[batt(X1,X2)∨emp(X2)]][pf(X1),[X1=b∨X2=c∨emp(X2)]][pf(X1),X1=b]∨[pf(X1),[X2=c∨emp(X2)]]Therstdisjunctgivesanswer({pf(t)},),foranyt=b;forthesecond,wehave={pf(t),emp(c)},foranytinourlanguage.
2SoundnessandCompletenessTheorem1(Soundness)LetT,IC,AbbeanabductiveprogramandGagoal.
(1)SupposerewritingfromX.
G∧ICgeneratesΘ(E∨Φ)suchthat(,σ)isextractedasananswertoG,basedonE.
Then,T∪comp()∪CET|=Gσ∧XIC.
(2)IfrewritingfromX.
G∧ICgeneratesF,thenT∪CET∪XIC|=G.
Proof.
(1)FromProposition1,ourassumptionthatX∩V(G)=,andthatcomp()|=EE,wehaveT∪comp()∪CET|=Gσ∧XICΘ(E∨Φ)σ.
SinceCET|=ΘEσ,and|=ΘEσ→Θ(E∨Φ)σ,wehaveT∪comp()∪CET|=Gσ∧XIC.
(2)Fromcomp(P)∪CET|=X(G∧IC)F,wegetcomp(P)∪CET∪XIC|=GbyourassumptionthatX∩V(G)introductionthenleadstocomp(P)∪CET∪IC|=G.
2Theorem2(Completeness)LetT,IC,Abbeanabduc-tiveprogramandGagoal.
Suppose(,σ)isananswertoGunder3-valuedlogic:T∪comp()∪CET|=3Gσ∧XIC.
Then,thereisaderivationfromX.
G∧ICtoagoalformulaΘ(E∨Φ),whereEisnotfurtherreduciblebyanydenedpredicates,suchthatananswer(,σ)canbeextracted,basedonE,whereisasubsetofandσismoregeneralthanσ.
Wecanprovethetheoremunderafairselectionrule,us-ingthewell-knownresultof(Kunen1987).
Thedifcultyforthe2-valuedcompletionsemanticsisknowntobecausedbyloops,e.
g.
,withT={pp},anygoalwouldfol-lowin2-valuedlogic.
Butin3-valuedlogic,Thasamodelwherepisundened,hencenonterminationofrepeatedun-foldingwouldnotresultinlossofcompleteness.
RelatedWorkandDiscussionOurapproachcanbeviewedasageneralizationoftheiffprocedureof(Fung&Kowalski1997),whichcomeswithavarietyofadditionalinferencerulesthatcanbeusedtomakeanswerextractionmoreconstructivefortheclassofallowedprogramsandgoals.
Aninterestingfactisthatourrewritesystemwithouttheseextrarulesdoesnotlosethecompletenessevenforarbitraryprogramsandgoals.
Onecansolvetheounderingqueryproblembyconstruc-tivenegation(CN)(see,e.
g.
,(Chan1988;Drabent1993;Stuckey1995)).
Alloftheseapproachesarebasedonthecompletionsemantics,andhavesimilarsoundnessandcom-pletenessresults.
Briey,ourapproachisconsiderablysim-pler,asitbuildsreasoningdirectlyoncompleteddenitionsonaatstructure,withoutrelyingonnestednitefailuretreesasneededinCN.
InrelatingtotheSLDNFAabductiveprocedure(De-necker&DeSchreye1998),wenotethatthecompletenessoftheirproceduredependsontheconditionthatderivationsterminate(duetonitefailure),whileoursdoesnot,simplybecausethereisnonotionofnitefailureinourapproach.
Oneadvantageofthecompletionsemanticsisthatiffdef-initionsarerstorderformulaswheretheoremhoodissemi-decidablesothatacompleteprocedureispossible.
Itisalsoknownthatifaprogramhasnoloops,thecompletionse-manticscoincideswiththeanswersetsemantics(Gelfond&Lifschitz1988).
Alloftheexamplenongroundprogramsinthispaperhavenoloops,soourrewritesystemprovesgoalsalsofortheanswersetsemantics.
E.
g.
,thetheoryTinExample1correspondstothefollowingprogramP:p(X)←notr(X,Y).
r(a,b).
Phasauniqueanswersetthatcontainsbothp(a)andp(b),andinfactp(t),foranytinthelanguage.
AsshowninExample1,thesearepreciselywhatareprovedfromthegoalp(V)byourrewritesystem.
NotethatPrologwouldfailthegoalp(V),duetoitsnaiveimplementationofnitefailure.
Furtherworkisneededtoaddressthreeissuesarisingfromthiswork.
TherstconcernsthepossibilityofreducingdependenciesofdisjunctsinagoalformulaΘ(E∨Φ),sothatΘEandΘΦmaybeprocessedindependently.
Wehaveshownthatinunfoldingnegativeliterals,certainuniversalvariablescanindeedbeconvertedtoexistentialones,thusreducingthechancesofshareduniversalvariables.
Thesec-ondissueisrelatedtothecomputationalpropertiesofsolv-ingquantiedequationsanddisequationsandthedesignofanefcientreasonerforit.
Finally,rewritestrategieswillbeanimportantissuetobeaddressedinfuturework.
AcknowledgementsFangzhenLin'sworkwassupportedinpartbyHKRGCCERG616806andbyNSFCgrant60496322.
ReferencesChan,D.
1988.
Constructivenegationbasedonthecom-pleteddatabase.
InProc.
ICLP/SLP,111–125.
Clark,K.
1978.
Negationasfailure.
LogicsandDatabases293–322.
Console,L.
;Theseider,D.
;andPorasso,P.
1991.
Onthere-lationshipbetweenabductionanddeduction.
J.
LogicPro-gramming2(5):661–690.
Denecker,M.
,andDeSchreye,D.
1998.
SLDNFA:anab-ductiveprocedurefornormalabductiveprograms.
J.
LogicProg.
34(2):111–167.
Drabent,W.
1993.
SLS-resolutionwithoutoundering.
InProc.
LPNMR'93,82–98.
Endriss,U.
;Mancarella,P.
;Sadri,F.
;Terreni,G.
;andToni,F.
2004.
TheCIFFprocedureforabductivelogicprogram-mingwithconstraints.
InJELIA'04.
Eshghi,K.
,andKowalski,R.
1989.
Abductioncomparedwithnegationbyfailure.
InProc.
6thICLP,234–254.
Fung,T.
,andKowalski,R.
1997.
Theiffproofprocedureforabductivelogicprogramming.
J.
LogicProgramming33(2):151–164.
Gelfond,M.
,andLifschitz,V.
1988.
Thestablemodelsemanticsforlogicprogramming.
InProc.
ICLP/SLP.
Kakas,A.
;Kowalski,R.
;andToni,F.
1995.
Theroleofabductioninlogicprogramming.
InHandbookofLogicinArticialIntelligenceandLogicProg.
OxfordUniversity.
Kakas,A.
;Michael,A.
;andMourlas,C.
2000.
ACLP:ab-ductiveconstraintlogicprogramming.
J.
LogicProgram-ming44:129–177.
Kunen,K.
1987.
Negationinlogicprogramming.
J.
LogicProgramming4(3):289–308.
Lin,F.
,andYou,J.
2002.
Abductioninlogicprogram-ming:anewdenitionandanabductiveprocedurebasedonrewriting.
ArticialIntelligence140(1/2):175–205.
Stuckey,P.
1995.
Negationandconstraintlogicprogram-ming.
Inf.
Comput.
118(1):12–33.