15-819K: Logic ProgrammingLecture 22HyperresolutionFrank PfenningNovember 14, 2006In this lecture we lift the forward chaining calculus from the ground tothe free variable case. The form of lifting required is quite different fro mthe backward chaining calculus. For Hor n logic, the result turns out to behyperresolution.22.1 Variables in Forwar d ChainingVariables in backward chaining in the style o f Prolog are placeholders forunknown terms. They are determined during unification, which occurswhen the head of a program clause is compared to t h e current goal.The same strategy d oes not seem appropriate for forward chaining. Asa first example, consider∀x. Q(x) ` Q(a).This violates the restrictions imposed for t h e last lecture, because x occursin the head of ∀x. Q(x) but not its body (which is empty).We cannot focus on the right-hand side since no Q( ) is in the context.But we can focus on the assumption, ∀x. Q(x). We have to guess a substi-tution term for x (which we will leave as a variable for now) and then blurfocus.∀x. Q(x), Q(X) ` Q(a)∀x. Q(x); Q(X)  Q(a)blurL∀x. Q(x); ∀x. Q(x)  Q(a)∀L∀x. Q(x) ` Q(a)focusLLECTURE NOTES NOVEMBER 14, 2006L22.2 HyperresolutionNothing within this focus ing sequence gives us a clue to what X should be.If we now focus on the right, we can se e in the second phase that X shouldbe a in order to complete th e proof.But is the set ∀x. Q(x), Q(X) actually saturated, or can we focus on∀x. Q(x) again? Since X is a placeholder, the proper interpretation of thesequent ∀ x. Q(x), Q(X) ` Q(a) should be:There exists an X such that ∀x. Q(x), Q(X) ` Q(a).Now it could be we need two instances of the universal quantifier, so wemight need to focus again on the left before anything else. An example ofthis is∀x. Q(x), Q(a) ⊃ Q(b) ⊃ Q0(c) ` Q0(c)So a priori there is no local consideration to rule out focusing again onthe left t o obtain the context ∀ x. Q(x), Q(X), Q(Y ), which is not redundantwith ∀x. Q(x), Q(X).By extension of this arg ument we s ee that we cannot bound the num-ber of times we need a universally qu antified assumption. This means wecan never definitively saturate the context. The existential interpretation ofvariables s eems somehow incompatible w ith forward chaining and satura-tion.22.2 Parametric AssumptionsLooking again at t h e d eduction steps∀x. Q(x), Q(X) ` Q(a)∀x. Q(x); Q(X)  Q(a)blurL∀x. Q(x); ∀x. Q(x)  Q(a)∀L∀x. Q(x) ` Q(a)focusLwe see that we lost a lot of information when blurring focus. We haveactually obtain Q (X) from the context w ithout any restriction on what Xis. In other words, we have really derived “For any X, Q(X)”. When w eadded it back to the context, it became existentially quantified over thesequent : “For some X, . . . , Q(X) ` . . .”.It w ould make no sense to exploit this genericity of X by restoring theuniversal quantifier: we already know ∀x. Q(x). Moreover, we would beintroducing a connective during bottom-up reasoning which would violateall principles of p roof search we have followed so far.LECTURE NOTES NOVEMBER 14, 2006Hyperresolution L22.3So we need to capture the fact that Q(X) holds for any X in the formof a judgment. We write ∆ ` Q where ∆ is a context of variables. In atyped se tting, ∆ records the types of all the variables, but we ignore thisslight g eneralization here. Now we have two forms of assumptions A and∆ ` Q. We call the latter parametric hypotheses or assumptions parametric in∆. There is no need to allow general parametric ass umptions ∆ ` A, al-though research on contextual modal type theory suggests that this wouldbe possible. The variables in ∆ in a parametric assumption ∆ ` Q s h ould beconsidered bound variables with scope Q.Parametric hypotheses are introduced in the blurring step.Γ, (∆ ` Q) ` Q0∆ = FV(Q)Γ; Q  Q0blurLWe assume here that the sequent does not contain any free variables othe rthan th ose in Q. Because for the moment we are only interested in forwardchaining, this is a reasonable assumption. We discuss the issue of saturationbelow.Now we consider the ot h er rules of the focusing system, one by one, tosee how to accomodate parametric hypotheses. We are restricting attentionto the Horn fragment with only synchronous ato ms.We now rule out (non-parametric) assumptions Q and just allow (∆`Q).Closed assumptions Q are silently interpreted as (· ` Q).The focusL rule is as before: we can focus on any non-parametric A. Bythe syntactic restriction, this cannot be a Q, so we elide the side condition.A ∈ Γ Γ; A  QΓ ` QfocusLThe impliesL rule also remains the same.Γ  Q1Γ; A2 QΓ; Q1⊃ A2 Q⊃LFor the ∀L rule we have to guess the substitution term t for x. This term tmay contain some fre e variables that are abstracted in the blur step.Γ; A(t/x)  QΓ; ∀x. A  Q∀LIn the implement ation t will be determined by unification, and we thenabstract over the remaining free variables.LECTURE NOTES NOVEMBER 14, 2006L22.4 HyperresolutionFocusing on the right is as before; the change appears in the identityruleΓ  QΓ ` QfocusR(∆ ` Q0) ∈ Γ Q0θ = Q dom(θ) = ∆Γ  QidLRight focus on Q s till fails if there is no appropriate (∆ ` Q0) and θ.22.3 Unification and GeneralizationAs a next step, we make the unification that happens during forward chain-ing fully explicit. Th is is the n atu r al exten sion of matching dur ing groundforward chaining discussed in the last lecture.A ∈ Γ Γ; A  QΓ ` QfocusLΓ  Q1| θ Γ; A2θ  QΓ; Q1⊃ A2 Q⊃LΓ; A(X/x)  Q X /∈ FV(Γ, A, Q)Γ; ∀x. A  Q∀L(∆ ` Q0) ∈ Γρ renaming on ∆Q0ρ.= Q | θΓ  Q | θidLno rule if no such ∆ ` Q0, θΓ  Q | θΓ  Q | (·)Γ ` QfocusRΓ, (∆ ` Q0) ` Q ∆ = FV(Q0)Γ; Q0 QblurLWe do no t permit free variables in Q for a global goal Γ ` Q. This may bereasonable at least on the Horn fragment if the renaming ρ always choosesfresh variables, since during forward chaining we never focus on the rightexcept to complete the proof.Reconsider an earlier example to see this system in action.∀x. Q(x), Q(a) ⊃ Q(b) ⊃ Q0(c) ` Q0(c)We must focus on ∀x. Q(x), which adds y ` Q(y) to the context.∀x. Q(x), Q(a) ⊃ Q(b) ⊃ Q0(c), (y ` Q(y)) ` Q0(c)Now we can focus on the second assumption, using substitutions a/y andb/y for the two premisses and adding · ` Q0(c) to the context. Now we canfocus on the right to prove Q0(c).LECTURE NOTES NOVEMBER 14,