Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

pages

English

Documents

Écrit par
Kaustuv Chaudhuri

Publié par
chaeh

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

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

Publié par

chaeh

Nombre de lectures

Langue

English

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:ingpolaritiescancharacterisetheeﬀectofMSTwithoutneedingtotransform15: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].Thediﬀerenceinthesediametrically25: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:ﬁcientlygeneralthatallstaticpolarityassignmentsarecomplete[8,1].Thetwoassign-35:mentsmaybefreelymixedfordiﬀerentatoms,whichwillproducehybridstrategies.36:Theproofsare,ofcourse,verydiﬀerent:oneassignmentmayadmitexponentialderiva-37:tionsofFibonaccinumbers,whiletheothermighthaveonlythelinearproofs.Even38:moreimportantly,thesearchspaceforproofsiswildlydiﬀerentfordiﬀerentassign-39:ments.Sometimestheassignmentcanbemadeeasily;forexample,atomsthatareused1

Voir