# Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

By

### chaeh

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
Tags :
-
-
-
##### Better Than
Origin : lix.polytechnique.fr
Number of pages: 16
See more See less
Deﬁnition5Environments(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)fortheformulaformedbyreplacingtheinEwithA,assumingitis352:syntacticallyvalid.AnenvironmentEiscalledpositive(resp.negative)ifE(p)(resp.353:E(n))issyntacticallyvalidforanypositiveatomp(resp.negativeatomn).354:Deﬁnition6(polarityassignment)WewriteA[at~+](resp.A[at~←−])tostand355:forthepositive(resp.negative)polarityassignmenttotheunpolarisedatomat~inthe356:formulaA.Ithasthefollowingrecursivedeﬁnition: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:Thisdeﬁnitionisextendedinthenaturalwaytocontexts,(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:becausetheonlywaytoproceedfurtherontheﬁrstpremiseiswiththeprrule.This369:instantiatesΓwithΓ,a+s.Ifwenowassignanegativepolaritytocst,wewouldobtain370:therule:Γ,C00,a+s`[bt],C00,a+s;∙`∙;cstΓ11

12/1000 maximum characters.

You may also like

from chaeh

from chaeh

from chaeh

next