Cet ouvrage et des milliers d'autres font partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour les lire en ligne
En savoir plus

Partagez cette publication

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
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin