Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

By
Published by

Niveau: Supérieur
version 1.0, compiled 2010-06-18 23:23 Magically Constraining the Inverse Method with1: Dynamic Polarity Assignment2: Kaustuv Chaudhuri3: INRIA Saclay, France4: : Abstract. Given a logic program that is terminating and mode-correct in an6: idealised Prolog interpreter (i.e., in a top-down logic programming engine), a7: bottom-up logic programming engine can be used to compute exactly the same8: set of answers as the top-down engine for a given mode-correct query by rewrit-9: ing the program and the query using the Magic Sets Transformation (MST). In10: previous work, we have shown that focusing can logically characterise the stan-11: dard notion of bottom-up logic programming if atomic formulas are statically12: given a certain polarity assignment. In an analogous manner, dynamically assign-13: ing polarities can characterise the effect of MST without needing to transform14: the program or the query. This gives us a new proof of the completeness of MST15: in purely logical terms, by using the general completeness theorem for focusing.16: As the dynamic assignment is done in a general logic, the essence of MST can17: potentially be generalised to larger fragments of logic.18: 1 Introduction19: It is now well established that two operational “dialects” of logic programming—top-20: down (also known as backward chaining or goal-directed) in the style of Prolog, and21: bottom-up (or forward chaining or program-directed

  • logic

  • forward chaining

  • dynamic polarity

  • well-moded

  • inverse method

  • global transformation

  • generally perform

  • such

  • better than


Published : Wednesday, June 20, 2012
Reading/s : 12
Origin : lix.polytechnique.fr
Number of pages: 16
See more See less
version1.0,compiled2010-06-1823:231:MagicallyConstrainingtheInverseMethodwith2:DynamicPolarityAssignment3:KaustuvChaudhuri4:INRIASaclay,France5:kaustuv.chaudhuri@inria.fr6:Abstract.Givenalogicprogramthatisterminatingandmode-correctinan7:idealisedProloginterpreter(i.e.,inatop-downlogicprogrammingengine),a8:bottom-uplogicprogrammingenginecanbeusedtocomputeexactlythesame9:setofanswersasthetop-downengineforagivenmode-correctquerybyrewrit-10:ingtheprogramandthequeryusingtheMagicSetsTransformation(MST).In11:previouswork,wehaveshownthatfocusingcanlogicallycharacterisethestan-12:dardnotionofbottom-uplogicprogrammingifatomicformulasarestatically13:givenacertainpolarityassignment.Inananalogousmanner,dynamicallyassign-14:ingpolaritiescancharacterisetheeectofMSTwithoutneedingtotransform15:theprogramorthequery.ThisgivesusanewproofofthecompletenessofMST16:inpurelylogicalterms,byusingthegeneralcompletenesstheoremforfocusing.17:Asthedynamicassignmentisdoneinagenerallogic,theessenceofMSTcan18:potentiallybegeneralisedtolargerfragmentsoflogic.19:1Introduction20:Itisnowwellestablishedthattwooperational“dialects”oflogicprogramming—top-21:down(alsoknownasbackwardchainingorgoal-directed)inthestyleofProlog,and22:bottom-up(orforwardchainingorprogram-directed)inthestyleofhyperresolution—23:canbeexpressedintheuniformlexiconofpolarityandfocusinginthesequentcalculus24:foragenerallogicsuchasintuitionisticlogic[8].Thedierenceinthesediametrically25:oppositestylesoflogicprogrammingamountstoastaticandglobalpolarityassignment26:totheatomicformulas.Suchalogicalcharacterisationallowsageneraltheoremprov-27:ingstrategyforthesequentcalculus,whichmightbebackward(goalsequenttoaxioms)28:asintableaumethodsorforward(axiomstogoalsequent)likeintheinversemethod,29:toimplementeitherforwardorbackwardchaining(oranycombination)forlogicpro-30:gramsbyselectingthepolaritiesfortheatomsappropriately.Focusedinversemethod31:provers,somesupportingpolarityassignment,havebeenbuiltforlinearlogic[4],intu-32:itionisticlogic[16],bunchedlogic[10]andseveralmodallogics[11]inrecentyears.33:Thecrucialingredientforthecharacterisationisthatpolaritiesandfocusingaresuf-34:ficientlygeneralthatallstaticpolarityassignmentsarecomplete[8,1].Thetwoassign-35:mentsmaybefreelymixedfordierentatoms,whichwillproducehybridstrategies.36:Theproofsare,ofcourse,verydierent:oneassignmentmayadmitexponentialderiva-37:tionsofFibonaccinumbers,whiletheothermighthaveonlythelinearproofs.Even38:moreimportantly,thesearchspaceforproofsiswildlydierentfordierentassign-39:ments.Sometimestheassignmentcanbemadeeasily;forexample,atomsthatareused1
40:toimplementactionsinastatetransitionsystemgenerallyperformbetterwhengiven41:anassignmentthatimplementsforwardchaining,whileatomsthatrepresentcomputa-42:tionalfunctionsperformbetterwithassignedtoimplementbackwardchaining.How-43:ever,thesituationisnotoftenthisclear,andstaticpolarityassignmenthasturnedoutto44:beacoarseandsomewhatunwieldytool,aswasnotedintheexperimentsin[8,16].45:Inthispaper,weproposetolookatdynamicpolarityassignmentasameanstodo46:betterthanstaticassignmentforcertainwellknownclassesofproblems.Dynamicas-47:signmentofaparticularformhasbeeninvestigatedbeforebyNigamandMiller[17]as48:ameansofincorporatingtablesintoproofobjects;however,theirnotionofdynamics49:involveschangestotheunderlyingproofsystem(suchastheadditionofcutsthatpo-50:larisecertaincutatomsindierentways).Weproposeinsteadtobuildaproofsystem51:thatretainsthesameinferencerulesasordinaryfocusing,butdynamicallyspecialises52:thembasedonpolarityassignmentsperformedatruntime.(Notethat“dynamicpolarity53:assignment”isnotaparticularalgorithmbutageneralclassofalgorithmsforcontrol-54:lingthesearchbehaviourofexistingalgorithms.Itisbesttothinkofitbyanalogywith55:orderingstrategiesinresolutiontheoremproving.)56:Inparticular,wegiveadynamicassignmentstrategythatimplementstheeectof57:theso-calledmagicsetstransformation[3,19,15],whichisaprogramtransformation58:constrainsforwardchainingtohavethesamesetofanswersasbackwardchaining.It59:isquitediculttoshowthatthetransformationhasthisintendedproperty.Moreover,60:sinceitisaglobaltransformationontheprogram,thatmighteven(inthegeneralcase)61:dependonthequery,itisnotmodularandcompositional.Wepropose,inthispaper,to62:giveanalternativepresentationofmagicsetsthatnotonlyavoidsthetransformation,63:butalsogivesacharacterisationofmagicsetsinthecommonlexiconoffocusing.That64:is,themagicsetsapproachisjustaspecialcaseofdynamicpolarityassignment,in65:muchthesamewayasforwardandbackwardchainingforHornclausesarejustspecial66:casesofstaticpolarityassignment.67:Welimitourattentioninthispapertothefocusedinversemethod[4]astheparticu-68:largeneralsearchstrategyforthesequentcalculus.Intuitively,thismethod“compiles”69:aclauseintoaninferenceruleasfollows:Γ`sumxyzsum(sX)Y(sZ):-sumXYZ.−→Γ`sum(sx)y(sz)70:Whenthisinferenceruleisreadfrompremisetoconclusion,theinterpretationisof71:forwardchainingonthecorrespondingclause.Suchrulescanberepeatedlyappliedto72:produceaninfinitenumberofnewsequentsdieringonlyinthenumberofss,which73:preventssaturationevenforquerieswithafinitebackwardchainingsearchspace.With74:suchclauses,forwardchainingcannotappealtonegationbyfailure,unlikebackward75:chaining.Weshowhowtousedynamicpolarityassignmenttoinsteadproduceanew76:sideconditiononsuchinferencerules:theconclusion(sum(sx)y(sz))mustbeneg-77:ativelypolarisedfortheruletobeapplicable.Theatomsarepolarisednegativelyby78:carefullyselectingonlythoseatomsthatareinthebaseofthelogicprogram.79:Oneimportantfeatureofthisre-investigationofthemagicsetsapproachisthat,be-80:causeitisperformedinamoregeneralcontext,wecanpotentiallygeneraliseittolarger81:fragmentsoflogicsuchastheuniformfragment.Moreover,sinceitdoesnotchangethe82:underlyingproofsystem,itcanpotentiallyco-existwithotherstrategies.Forexample,2
83:ifthedynamicassignmentalgorithmgetsstuck,theremainingatomscanbepolarised84:insomeotherfashionandtheinversemethodresumedwithoutlosingcompleteness.85:Therestofthispaperisorganisedasfollows.Insec.2themagicsetstransformation86:issketchedbywayofexample.Section3thensummarisesthedesignofthefocused87:inversemethodandstaticpolarityassignment.Section4introducesdynamicpolarity88:assignmentandshowshowtouseittoimplementthemagicsetsrestriction(sec.4.2).89:Finally,sec.5discussestheconclusionsandscopeoffutureworkondynamicpolarity90:assignment.91:2MagicSetsTransformation92:ThissectioncontainsaquickoverviewoftheMagicSetsTransformationforlogicpro-93:grams.Weusethe“core”versionpresentedin[15],whichislessgeneralthansome94:otherdesignsintheliterature[3,19]butalsoeasiertoexplainandreasonabout.The95:logicprogramswewillconsideraremadeupofHornclausesandsatisfyaglobalwell-96:modednesscriterion.97:Definition1(Hornclauses)AHornclauseisaniteratedimplicationofatomicformu-98:lasthatisimplicitlyclosedoverallitsvariables.Thatis,Hornclauses(C,D,...)satisfy99:thefollowinggrammar: C,D,...Fat~ a~tCt,s,...Fx ft~100:wherearangesoverpredicatesymbols,foverfunctionsymbols,andxovervariables.101:Thenotationt~standsforalist,possiblyempty,ofterms.102:ManyextensionsofthisdefinitionofHornclausesexistintheliterature,buttheyare103:allgenerallyequivalenttothisfragment.Alogicprogramisjustanunorderedcollection104:ofHornclauseswhereeachpredicateandfunctionsymbolhasauniquearity.(Wedo105:notconsiderparticularorderingsoftheclausesbecausewearenotinterestedinthe106:preciseoperationalsemanticsofalogicprogramminglanguagesuchasProlog.)107:Definition2(moding)Everypredicatesymbolofarityncanbeassignedamode,108:whichisastringoflengthncomposedofthecharactersiando,whicharemnemonics109:for“input”and“output”respectively.Amodeassignmenttoallpredicatesinalogic110:programiscalledamoding.Theinputsofapredicatewithrespecttoamodearethose111:argumentscorrespondingtotheoccurrencesofiinthemode;likewise,theoutputsare112:theargumentscorrespondingtoointhemode.113:Definition3(well-modedness)Allthefollowingarewithrespecttoagivenmoding:114:Agoalqueryiswell-modediitsinputsareground.115:Aclausea1t~1→∙∙∙→ant~nbs~iswell-modediforalli1..n,thevariables116:intheinputsofait~iarecontainedintheunionofthevariablesintheoutputsof117:ajt~jfori<jnandofthevariablesintheinputsofbs~.118:Alogicprogramiswell-modedieveryclauseinitiswell-moded.3
119:Thedefinitionofwell-modednessfornon-unitclausesintuitivelystatesthat,ina120:right-to-leftreadingoftheclause,theinputsofanatomicformulamustbedefinedthe121:outputsofearlieratomicformulasandtheinputsofthehead.Thereisnofundamental122:needtoreadthebodyoftheclausefromrighttoleft;indeed,well-modednesscanbe123:generalisedtoallowforanypermutationofthebodytosatisfytheinclusioncriteriafor124:inputvariables.Givenawell-modedprogramandquery,everyderivationofaninstance125:ofthequeryfromtheprogramwillbeground(fortheproof,see[2]).126:Weusethesamemotivatingexamplefrom[15]:computingthesumoftheelements127:ofalistofnaturalnumbers.TheclausesoftheprogramareasfollowsinPrologstyle.128:(*modelsum=io*)129:lsum[]0.130:lsum(X::Y)k:-lsumYJ,sumXJK.131:(*modesum=iio*)132:sum0XX.133:sum(sX)Y(sZ):-sumXYZ.134:Thisprogramiswell-modedbecausetheoutputsflowintotheinputsfromlefttoright135:inthebodyoftheclauses.Aquerysuchas?-lsum[1,2,3]Xiswell-moded136:becausetheinputisground,whileaquerysuchas?-lsumX20isnotwell-moded.137:Toproveawellmodedquery,thebackwardchainingortop-downlogicprogram-138:mingapproachmatchesthegoalwiththeheadsoftheclausesintheprogram,andfor139:eachsuccessfulmatch,replacesthegoalwiththematchedinstanceofthebodyofthe140:clauseasnewsubgoals.Awell-modedprogramissaidtobeterminatingifthereareno141:infinitebackwardchainingderivationsforawell-modedquery.142:Theforwardchainingorbottom-uplogicprogrammingstrategystartsfromtheunit143:clausesintheprogram,matchesthebodyofaclausewiththeseclauses,andaddsthe144:mostgeneralinstanceofthematchedheadasanewclause.Thisisiterateduntil(a145:generalisationof)thegoalqueryisderived.Thisdirectionisnotquiteasobviously146:goal-directedasbackwardchaining,butithasmanyfundamentalmerits.Itbuildsa147:databaseofcomputedfactsthatareallmutuallynon-interfering,andthereforerequires148:nobacktrackingorglobal,statefulupdates.Moreover,factsandthereforederivations149:areimplicitlyshared,sotheloopdetectionissuethatplaguesbackwardchainingdoes150:notapplyhere.151:However,forwardchainingsuersfromtheobviousproblemthatitover-approximates152:thequery,performingalotofwastefulsearch.Fortunately,itispossibletoconstrainfor-153:wardchainingforagivenprogramandquerysuchthatthealgorithmwillsaturate,i.e.,154:reachastatewherenonewfactscanbegenerated,ithequeryterminatesinbackward155:chaining.Thisisachievedbyrewritingtheprogramandthequerysothattheforward156:algorithmapproximatesbackwardsearch.157:Thecommonelementoftheapproachestoconstrainforwardchainingisthenotion158:ofamagicset,whichisanabstractrepresentationofthebaseoftheprogram[15].159:Weshallillustrateitherewiththeexampleabove.Foreachpredicatea,anewmagic160:predicatea0isaddedthathasthesamearityastheinputarityoftheoriginalpredicate.161:Then,eachclauseoftheprogramistransformedtodependonthemagicpredicate162:appliedtotheinputsofthehead.Thatis,weobtainthefollowingrewrittenclauses:4
163:lsum[]0:-lsum’[].164:lsum(X::Y)k:-lsum’(X::Y),lsumYJ,sumXJK.165:sum0XX:-sum’0X.166:sum(sX)Y(sZ):-sum’(sX)Y,sumXYZ.167:Astherearenolongeranyunitclauses,forwardchainingcannotbeginwithoutsome168:additionalinput.Thisisprovidedintheformofthemagicversionofthegoalqueryas169:anewunitclause:170:lsum’[1,2,3].171:Finally,clausesareaddedforthemagicpredicatestopropagateinformationaboutthe172:base.Foreachnon-unitclause,thereisonepropagationruleforeachpredicateinthe173:bodyoftheclause.Forthisexample,wewouldhave:174:lsum’Y:-lsum’(X::Y).175:sum’XJ:-lsum’(X::Y),lsumYJ.176:sum’XY:-sum’(sX)Y.177:Forwardchainingonthistransformedprogramwillcomputethesameinstancesofthe178:queryasbackwardchainingontheoriginalprogramandquery.179:Correctnessofthismagicsetstransformationisgenerallyquitediculttoprove.180:OneofthemostreadableproofswasprovidedbyMascellanietal[15];thatpaperalso181:containsafullyformaldefinitionofthetransformationandanumberofotherexamples.182:However,alltransformationalapproachessuerfromthesameproblemsoutlinedinthe183:introduction:theyrequiredrastic,non-modular,andnon-compositionalmodificationsto184:theprogram.Intherestofthepaperwewillgiveadierentexplanationofthemagic185:setstransformationthatdoesnotsuerfromtheseproblems,andismoreovermanifestly186:correctbecauseofverygeneralprooftheoreticpropertiesoffocusedsequentcalculi.187:3TheFocusedInverseMethod188:Inthissectionwereviewthefocusedinversemethodforintuitionisticlogic.Mostofthe189:materialofthissectionhasalreadyappearedinin[4,8,16,9]andinreferencesthere-190:from.Likeotherrecentaccountsofintuitionisticfocusing[16,6],weadoptapolarised191:syntaxforformulas.Intuitively,positiveformulas(i.e.,formulasofthepositivepolar-192:ity)arethoseformulaswhoseleftsequentrulesareinvertibleandnegativeformulas193:arethosewhoserightrulesareinvertible.Everypolarisedlogicalconnectiveisunam-194:biguouslyinoneofthesetwoclasses.Inordertopreventanoverlap,wealsoassign195:theatomicformulastooneofthetwoclasses.Anypolarityassignmentfortheatomsis196:complete[8].197:Definition4(syntax)Wefollowthisgrammar: P,QFp PQ 1 PQ 0 x.P NN,MFn N&M > P(N x.N P pF at~,+ nF at~, PFP nN+FN p198:Formulas(A,B,...)areeitherpositive(P,Q,...)ornegative(N,M,...).5
199:Atomicformulas(oratoms)(p,q,n,m,...)arealsopolarised.Eachatomconsists200:ofanatomicpredicate(a,b,...)appliedtoa(possibly empt y)listofterms,anda201:polarity.Weshallsometimesabusenotationandwriteat~,±asa±t~,eventhough202:itistheatomandnotthepredicatethatcarriesthepolarity.203:Leftpassiveformulas(N+,M+,...)andrightpassiveformulas(P,Q+,...)are204:usedtosimplifythenotationslightly.205:Weuseconnectivesfrompolarisedlinearlogicinsteadofthemoreusualintuition-206:isticconnectivestomakethepolaritiesexplicit.Thepolarityswitchingconnectives207:andareonlybureaucraticanddonotchangethetruthvalueoftheiroperands.Both208:and&havethesametruthvalueastheusualintuitionisticconjunction—thatis,209:ABA&Bifweignorepolaritiesandomittheswitchingconnectivesand—just210:dierentinferencerules.Inotherformulationsofpolarisedintuitionisticlogicthesetwo211:polarisationsofconjunctionaresometimeswrittenas+or[14],butwepreferthe212:familiarnotationfromlinearlogic.Likewise,hasthesametruthvalueasand(213:thesametruthvalueas.214:Theinferencesystemforthislogicwillbegivenintheformoffocusedsequent215:calculusrules[1,16].Wehavethefollowingkindsofsequents:Γ`[P]right-focusonPΓ;[N]`Qleft-focusonN;N216:Γ;Ω`left-activeonΩandright-activeonNQ;| {z }γ 217:where:ΓF Γ,NiscalledthepassivecontextandΩF Ω,Pistheactivecontext.218:Bothcontextsareinterpretedasmultisets(admitsonlyexchange).Weusetheusual219:conventionofdenotingmultisetunionwithcommas.Itwillturnoutthatthepassive220:contextisalsoaset,butwewillprovethisasanadmissibleprincipleinsteadofwriting221:explicitrulesofweakeningandcontraction.NotethereforethatΓ1,Γ2isnotthesame222:asΓ1Γ2;whenthelatterinterpretationisneeded,itwillbewrittenexplicitly.223:ThefocusedsequentcalculuswillbepresentedinastylisticvariantofAndreoli’s224:originalformulation[1].Thefullsetofrulsisinfig.1.Ithasanintensionalreadingin225:termsofphases.AttheboundariesofphasesaresequentsoftheformΓ;∙`∙;Q,226:whichareknownasneutralsequents.Proofsofneutralsequentsproceed(readingfrom227:conclusiontopremises)asfollows:228:1.Decision:afocusisselectedfromaneutralsequent,eitherfromthepassivecontext229:orfromtheright.Thisfocusedformulaismovedtoitscorrespondingfocusedzone230:usingoneoftherulesdlordr(d=“decision”,andr/l=“right”/“left”).Theleft231:rulecopiesthefocusedformula.232:2.Focusedphase:foraleftorarightfocusedsequent,leftorrightfocusrulesare233:appliedtotheformulaunderfocus.Thesefocusedrulesareallnon-invertibleinthe234:(unfocused)sequentcalculusandthereforedependonessentialchoicesmadeinthe235:proof.Thisisfamiliarfromfocusingforlinearlogic[1,8].236:3.Activephase:oncetheswitchrulesrandlareapplied,thesequentsbecome237:activeandactiverulesareapplied.Theorderoftheactiverulesisimmaterialas6
ΓΓ(right-focus);∙`N;Γ,p`pprΓ;[N]rΓ`[P]Γ`[Q]Γ`[Pi]Γ;[P[t/x]]Γ`[PQ]rΓ`[1]1rΓ`[P1P2]riΓ;[x.P]r(left-focus)Γ;P`∙;QΓ;[n]`nnlΓ;[P]`QlΓ;[Ni]`QΓ`[P]Γ;[N]`QΓ;[N[t/x]]`QΓ;[N1&N2]`Q&liΓ;[P(N]`Q(lΓ;[x.N]`Ql(active);Ω`∙;nnrΓ;Ω`∙;PrΓ;Ω`N;Γ;Ω`M;&r;Ω`n;Γ;Ω`↑P;Γ;Ω`N&M;Γ;Ω,P`N;Γ;Ω`N[a/x];Γ;Ω`>;>rΓ;Ω`P(N;(rΓ;Ω`∀x.N;ra,pt~;Ω`γplΓ,N;Ω`γlΓ;Ω,P,Q`γlΓ;Ω`γ1l;Ω,pt~`γΓ;Ω,N`γΓ;Ω,PQ`γΓ;Ω,1`γΓ;Ω,P`γΓ;Ω,Q`γl0lΓ;Ω,N[a/x]`γlaΓ;Ω,PQ`γΓ;Ω,0`γΓ;Ω,x.N`γ(decision)Γ`[P]Γ,N;[N]`QΓ;∙`∙;PdrΓ,N;∙`∙;QdlFig.1.Focusedsequentcalculusforpolarisedfirst-orderintuitionisticlogicΓΓΓ238:allorderingswillproducethesamelistofneutralsequentpremises.InAndreoli’s239:systemtheirrelevantnon-determinismintheorderoftheseruleswasremovedby240:treatingtheactivecontextΩasordered;however,wedonotfixanyparticular241:ordering.242:Thesoundnessofthiscalculuswithrespecttoanunfocusedsequentcalculus,suchas243:Gentzen’sLJ,isobvious.Forcompleteness,werefertheinterestedreadertoanumber244:ofpublishedproofsintheliterature[8,13,18,12].245:Thepurposeofstartingwithapolarisedsyntaxandafocusedcalculusisthatweare246:abletolookatderivedinferencerulesforneutralsequentsasthebasicunitofsteps.For247:instance,oneofthederivedinferencerulesfortheformulaN,pq(m&(l(n)248:inthepassivecontextisgiveninfig.2.Theinstanceofpraboveforcesptobeinthe249:passivecontextbecausethatistheonlyrulethatcanbeappliedtocontructasequent250:oftheformΔ`p.Likewise,thenlruleforcestherighthandsideoftheconclusion251:sequenttobethesameastheleftfocusedatomn.Finally,thedlrulerequiresNto252:alreadybepresentinthepassivecontext.253:Asweobserve,focusingcompilesformulassuchasNabove,whichmaybeclauses254:inaprogram,into(derived)inferencerules.Focusingcanalsoproducenewfacts,which255:areneutralsequentsthathavenoopenpremisesafterapplyingaderivedinferencerule.7
ΓΓΓΓ,N,p;∙`∙;l,N,p;∙`l;nlprΓ,N,p`[l]Γ,N,p;[n]`n,N,p`pΓ,N,p;[l(n]`n,N,p`pqΓ,N,p;[m&(l(n)]`n&l2Γ,N,p;[N]`ndli.e.,Γ,N,p;∙`∙;l,N,p;∙`∙;nΓ,N,p;∙`∙;nFig.2.OnederivedinferenceruleforN.Γ256:Anexamplewouldbethecaseforthederivationabovewhere,insteadof&l2wewere257:touse&l1.InthiscasewewouldobtainthefactΓ,N,p;∙`∙;m.Ifthegoalwereof258:thisform,wewouldbedone.259:Thispropertyoffocusingcanbeexploitedtogiveapurelyproof-theoreticexpla-260:nationforcertaindialectsofproofs.ForHornclauses,considerthecasewhereallthe261:atomsarenegative,i.e.clausesareoftheformx~.m1(∙∙∙(mj(n.Ifclausewere262:namedN,thenitsderivedinferenceruleis:Γ,N;∙`∙;m1[t~/x~]∙∙∙Γ,N;∙`∙;mj[t~/x~]Γ,N;∙`∙;n[t~/x~]263:Sincethecontextisthesameinallpremisesandtheconclusion,weneedonlylook264:attherighthandside.Ifwereadtherulefromconclusiontopremises,thenthisrule265:implementsback-chainingfromaninstanceoftheheadofthisHornclausetothecor-266:respondinginstancesofthebodyoftheclause,wheretheneutralsequentsrepresent267:thecurrentlistofsub-goals.Thus,thegeneraltop-docnlogicprogrammingstrategy(or268:backwardchaining)consistsofperforminggoal-directedfocusedproofsearchonHorn269:clauseswithnegativeatoms.Iftheatomswereallassignedpositivepolarityinstead,270:thenthesamegoal-directedfocusedproofsearchwouldperformakindofbottom-up271:logicprogramming(orforwardchaining).Staticpolarityassignmentfortheatomsis272:thereforealogicalcharacterizationofforwardandbackwardchainingstrategies.In-273:deed,iftheatomswerenotuniformlygiventhesamepolarities,thenthefocusedproofs274:wouldbeamixtureofforwardandbackwardchaining.275:3.1Forwardreasoningandtheinversemethod276:Animportantpropertyofthesequentcalculusoffig.1isthatthereisastructuralcut-277:eliminationalgorithm[8];asaconsequence,thecalculusenjoysthesubformulaprop-278:erty.Indeed,itispossibletostatethesubformulapropertyinaverystrongformthat279:alsorespectsthesignofthesubformula(i.e.,whetheritisprincipalontheleftorthe280:rightofthesequent)andtheparametricityofinstances(i.e.,thesubformulasofaright281:oraleftcanberestrictedtogenericinstances).Weomitadetaileddefinitionand282:proofherebecauseitisastandardresult;seee.g.[7]forthedefinition.283:Thebenefitofthestrongsubformulapropertyisthatwecanrestricttherulesoffig.1284:tosubformulasofagivenfixedgoalsequent.Withthisrestriction,itbecomespossibile8
285:toapplytheinferencerulesinaforwardmanner,frompremisestoconclusion.The286:inputsofsuchaforwardreasoningstrategywouldbethefactsthatcorrespondtofocus-287:ingonthepassiveformulasandoperandsoftheswitchconnectivesinthegoalsequent,288:subjecttothesubformularestriction.Thatis,weadmitonlythoseinitialsequents(in289:therulesprandnl)wheretheprincipalatomicformulaisbothaleftandarightsigned290:subformulaofthegoalsequent.Fromtheseinitialsequentsweapplythe(subformula-291:restricted)inferencerulesforwardinaforwardmanneruntilwederive(ageneralisation292:of)thegoalsequent.293:Inorderforthiskindofforwardsearchstrategytobeimplementable,thereneedsto294:besomefurthermodificationstotheinferencerules.Firstly,theruleschemasmustbe295:restrictedtoremoveelementsthatdonotoccurinthepremises.Forinstance,therule296:1rbisreplacedwith1rfbecausethecontextΓisnotpresentamongthepremises:Γ`[1]1rb∙`[1]1rf297:(Thesuxesbandfareusedtodistinguishbackwardfromforwardrules.)Asaresult298:ofthistransformation,thecontextsinthepremisesofbinaryrulesnolongermatchup299:exactly,andsotheyarejoinedinmultisetunionsuchas:Γ1`[P]Γ2`[Q]Γ1,Γ2`[PQ]rf300:Wethenaddanexplicitruleoffactoringtogetridofduplicatesintheneutralsequents:Γ,N+,N+;∙`∙;δfΓ,N+;∙`∙;δ301:whereδisoftheformorQ.Tocompletethedesign,wethenliftthegroundcalculus302:tofreevariablesandrelaxidentityinrulessuchasprandnltounifiability,andcompute303:onlymostgeneralinstancesofnewsequents.Thiscoredesignofaforwardversionof304:abackwardsequentcalculusisawellknown“recipe”outlinedintheHandbookarticle305:ontheinversemethod[9].306:Oneoptimisationnotmentionedin[9]butimplementedinmanyinversemethod307:provers[4,16]isglobalisation:theforwardversionofthedlruleisspecializedintothe308:followingtwoforms:Γ;[N]`δN<Γ0dlfΓ;[N]`δNΓ0dlfΓ,N;∙`∙;δ1Γ;∙`∙;δ2309:whereΓ0isthepassivecontextofthegoalsequent.Thiscontextispresentinevery310:sequentinthebackwardproof,sothereisnoneedtomentionitexplicitlyintheforward311:direction.Forlogicprograms,Γ0willcontaintheclausesoftheprogramanditisnot312:importanttodistinguishbetweentwocomputedsequentsthatdieronlyintheused313:clausesoftheprogram.314:Letusrevisitthestaticpolarityassignmentquestionintheforwarddirection.The315:forwardderivedrulefortheHornclausex~.m1(∙∙∙(mj(nΓ0,afterlifting316:tofreevariables,is:1;∙`∙;m10∙∙∙Γj;∙`∙;m0jθ=mgu(hm1,...,mji,hm10,...,m0ji)(Γ1,...,Γn;∙`∙;n)[θ]Γ9
317:Forunitclauses,whichprovidetheinitialsequents,thepassivecontextΓisempty318:(becausetherearenopremisesremainingafterglobalisation).Therefore,allneutral319:sequentscomputedbyforwardreasoningwillhaveemptypassivecontexts,givingus320:therule:;∙`∙;m10;∙`∙;m0jθ=mgu(hm1,...,mji,hm10,...,m0ji)(;∙`∙;n)[θ]321:Thus,thisderivedinferenceruleimplementsforwardchainingforthisclause.Thissit-322:uationisdualtothebackwardreadingoftherulesoffig.1whereastaticnegative323:assignmenttotheatomsimplementedbackwardchaining.Asexpected,astaticpos-324:itivepolarityassignmenttotheatomsimplementsbackwardchainingintheforward325:calculus.Thetechnicaldetailsofoperationaladequacycanbefoundin[8].326:4DynamicPolarityAssignment327:Theprevioussectiondemonstratesthatwecanimplementforwardchaining(orbottom328:uplogicprogramming)usingthevocabularyoffocusingandpolarityassignment.For329:therestofthispaperweshalllimitorattentiontoforwardreasoningastheglobal330:strategy,withnegativepolarityassignmentfortheatomsasourmeansofimplementing331:forwardchaining.332:Obviouslythebenefitofpolarityassignmentisthatcompletenessisatrivialcon-333:sequenceofthecompletenessoffocusingwithrespecttoanyarbitrary,evenheteroge-334:neous,polarityassignmentfortheatoms.Moreover,thecompletenessoftheivnerse335:methodmerelyrequiresthattheruleapplicationstrategybefair.Thisminimalrequire-336:mentoffairnessdoesnotforceustoassignthepolarityofallallatomsstatically,as337:longaswecanguaranteethateveryatomthatisrelevanttotheproofiseventuallyas-338:signedapolarity(andthattherestoftheinversemethodengineisfair).Canwedo339:betterthanstaticassignmentwithdynamicassignment?Thissectionwillanswerthis340:questionarmatively.341:4.1Themechanismofdynamicpolarityassignment342:Letuswriteunpolarisedatoms(i.e.,atomsthathaven’tbeenassignedapolarity)simply343:intheformat~,andallowthemtobeusedasbothpositiveandnegativeformulasinthe344:syntax.Thatis,weextendthesyntaxasfollows: P,Q,...Fat~ p PQ 1 PQ 0 x.P N N,M,...Fat~ n N&M > P(N x.N P345:Forexample,AHornclausewithunpolarisedatomshavethesyntaxx~.a1t~1(∙∙∙(346:ajt~j(bs~wherethex~arethevariablesthatoccurinthetermst~1,...,t~j,s~.347:Consideravariantofthefocusedinversemethodwhereweallowtwokindsof348:premisesforinferencerules:neutralsequentsasbefore,andsequentsthathaveafocus349:onanunpolarisedatomwhichwecallprotosequents.Aninferencerulewithproto350:sequentpremiseswillbecalledaprotorule.01
Definition5Environments(E,F,...)aregivenbythefollowinggrammar: E,...FP Q P,Q,...F P⊗Q P⊗Q P⊕Q P⊕Q x.P ↓N N,M,...F N&M N&M P(N P(N x.N ↑P351:WewriteE(A)fortheformulaformedbyreplacingtheinEwithA,assumingitis352:syntacticallyvalid.AnenvironmentEiscalledpositive(resp.negative)ifE(p)(resp.353:E(n))issyntacticallyvalidforanypositiveatomp(resp.negativeatomn).354:Definition6(polarityassignment)WewriteA[at~+](resp.A[at~←−])tostand355:forthepositive(resp.negative)polarityassignmenttotheunpolarisedatomat~inthe356:formulaA.Ithasthefollowingrecursivedefinition:357:Iftheunpolarisedatomat~doesnotoccurinA,thenA[at~←±]=A.358:IfA=E(at~)andEispositive,thenA[at~+]=(E(a+t~))[at~+]A[at~←−]=(E(at~))[at~←−]359:IfA=E(at~)andEisnegative,thenA[at~+]=(E(a+t~))[at~+]A[at~←−]=(E(at~))[at~←−]360:Thisdefinitionisextendedinthenaturalwaytocontexts,(proto)sequents,and(proto)361:rules.362:Polarityassignmentonprotorulesgenerallyhastheeectofinstantiatingcertain363:schematicmeta-variables.Forinstance,considerthefollowingproto-rulethatcorre-364:spondstoaleftfocusontheunpolarisedHornclauseC,x,y.ax(by(cxy:Γ,C`[as]Γ,C`[bt]Γ,C;[cst]`QΓ,C;∙`∙;Q365:Allthepremisesofthisruleareprotosequents.Supposeweassignapositivepolarity366:toas;thiswillchangetheprotoruleto:Γ,C`[a+s]Γ,C`[bt]Γ,C;[cst]`QΓ,C;∙`∙;Q367:(whereC0isC[as+]).Thisprotoruleactuallycorrespondsto:Γ,C0,a+s`[bt]Γ,C0,a+s;[cst]`QΓ,C0,a+s;∙`∙;Q368:becausetheonlywaytoproceedfurtheronthefirstpremiseiswiththeprrule.This369:instantiatesΓwithΓ,a+s.Ifwenowassignanegativepolaritytocst,wewouldobtain370:therule:Γ,C00,a+s`[bt],C00,a+s;∙`∙;cstΓ11
Be the first to leave a comment!!

12/1000 maximum characters.