Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

De
16 pages
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


Voir plus Voir moins

Vous aimerez aussi

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