Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

Kaustuv Chaudhuri

Description

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

Sujets

• Chaudhary
• Forward chaining
• Inverse method
• Better Than

Informations

• Publié par: chaeh
• Nombre de lectures: 12
• Langue: English

Extrait

version1.0,compiled2010-06-1823:23 1: MagicallyConstrainingtheInverseMethodwith 2: DynamicPolarityAssignment 3: KaustuvChaudhuri 4: INRIASaclay,France 5: [e-mail] 6: Abstract.Givenalogicprogramthatisterminatingandmode-correctinan 7: idealisedProloginterpreter(i.e.,inatop-downlogicprogrammingengine),a 8: bottom-uplogicprogrammingenginecanbeusedtocomputeexactlythesame 9: setofanswersasthetop-downengineforagivenmode-correctquerybyrewrit- 10: ingtheprogramandthequeryusingtheMagicSetsTransformation(MST).In 11: previouswork,wehaveshownthatfocusingcanlogicallycharacterisethestan- 12: dardnotionofbottom-uplogicprogrammingifatomicformulasarestatically 13: givenacertainpolarityassignment.Inananalogousmanner,dynamicallyassign- 14: ingpolaritiescancharacterisethee ff ectofMSTwithoutneedingtotransform 15: theprogramorthequery.ThisgivesusanewproofofthecompletenessofMST 16: inpurelylogicalterms,byusingthegeneralcompletenesstheoremforfocusing. 17: Asthedynamicassignmentisdoneinagenerallogic,theessenceofMSTcan 18: potentiallybegeneralisedtolargerfragmentsoflogic. 19: 1Introduction 20: Itisnowwellestablishedthattwooperational“dialects”oflogicprogramming—top- 21: down(alsoknownasbackwardchainingorgoal-directed)inthestyleofProlog,and 22: bottom-up(orforwardchainingorprogram-directed)inthestyleofhyperresolution— 23: canbeexpressedintheuniformlexiconofpolarityandfocusinginthesequentcalculus 24: foragenerallogicsuchasintuitionisticlogic[8].Thedi ff erenceinthesediametrically 25: oppositestylesoflogicprogrammingamountstoastaticandglobalpolarityassignment 26: totheatomicformulas.Suchalogicalcharacterisationallowsageneraltheoremprov- 27: ingstrategyforthesequentcalculus,whichmightbebackward(goalsequenttoaxioms) 28: asintableaumethodsorforward(axiomstogoalsequent)likeintheinversemethod, 29: toimplementeitherforwardorbackwardchaining(oranycombination)forlogicpro- 30: gramsbyselectingthepolaritiesfortheatomsappropriately.Focusedinversemethod 31: provers,somesupportingpolarityassignment,havebeenbuiltforlinearlogic[4],intu- 32: itionisticlogic[16],bunchedlogic[10]andseveralmodallogics[11]inrecentyears. 33: Thecrucialingredientforthecharacterisationisthatpolaritiesandfocusingaresuf- 34: ficientlygeneralthatallstaticpolarityassignmentsarecomplete[8,1].Thetwoassign- 35: mentsmaybefreelymixedfordi ff erentatoms,whichwillproducehybridstrategies. 36: Theproofsare,ofcourse,verydi ff erent:oneassignmentmayadmitexponentialderiva- 37: tionsofFibonaccinumbers,whiletheothermighthaveonlythelinearproofs.Even 38: moreimportantly,thesearchspaceforproofsiswildlydi ff erentfordi ff erentassign- 39: ments.Sometimestheassignmentcanbemadeeasily;forexample,atomsthatareused 1