User rob simmons - MathOverflow

Answer by Rob Simmons for Is forward chaining also a form of focusing?

2011-05-28T14:22:50Z

So the short answer is "yes, the forward chaining calculus is complete." Is forward-chaining still a form of focusing? Well, yes, though giving a logical characterization to saturation in forward-chaining is currently a point of investigation.

I think Kaustuv Chaudhuri was the first person to take Andreoli's observations about polarity and formally connect them to forward and backward chaining, though he did so in an unusual way (at least from my perspective, and, based on reading your question, from yours as well). In particular, Chaudhuri works from the perspective of the axioms-down (or inverse method) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in A Logical Characterization of Forward and Backward Chaining in the Inverse Method, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, Polarities in Theorem Proving and Logic Programming. Kaustuv might argue that the inverse method is one of the "better ways to formulate forward chaining than with (->L Forward)", though I don't exactly take this view (and don't want to put words in his mouth!)

I wrote some notes about this some time ago in a blog post called Focusing and Synthetic Rules that tried to re-cast some of Chaudhuri's observations from the perspective of bottom-up proof search. Also, in the (woefully-un-commented) Twelf Wiki article presenting a variant of the completeness-of-focusing proof that I sketched in the previous answer, I actually had some fun using the computational content of the completeness-of-focusing argument to actually transform proofs into forward-chaining form and backward-chaining form. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.

Answer by Rob Simmons for How establish conversion of cut-free proof into uniform proof?

2011-05-24T14:32:42Z

I think some of the commenters were confused by the notation $\Gamma \vdash A \downarrow B$, which I have only seen written as $\Gamma [ A ] \vdash B$ or $\Gamma \vdash A > B$. The downarrow comes, as you note in a comment, from Andreoli's notation, but that notation is more common in presentations of sequent calculi for classical logics, at least in my experience. The notation I'll use is the one with $>$ instead of $\downarrow$, which comes from Cervesato and Pfenning's "A Linear Spine Calculus."

Two proof systems

So, to restate the goal, we have the following sequent calculus for first-order, minimal logic:

$$ {P \in \Gamma \over \Gamma \Rightarrow P}{\it init} \qquad {\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{{\supset}R} \qquad {(A \supset B) \in \Gamma \qquad \Gamma \Rightarrow A \qquad \Gamma, B \Rightarrow C \over \Gamma \Rightarrow C}{{\supset}L} $$

$$ {\Gamma \Rightarrow A(\alpha) \over \Gamma \Rightarrow \forall x.A(x)}{{\forall}R^\alpha} \qquad {(\forall x.A(x)) \in \Gamma \qquad \Gamma, A(t) \Rightarrow C \over \Gamma \Rightarrow C}{{\forall}L} $$

We want to relate this proof system to the following presentation of "focused" or "uniform" proofs. I would argue that in your presentation above, the description of uniform proofs is missing at least one necessary rule ($\it focus$) and arguably is missing three; I would write the full system of focused (a.k.a. uniform) proofs as follows:

$${A \in \Gamma \qquad \Gamma \vdash A > P \over \Gamma \vdash P}{\it focus} \qquad {{} \over \Gamma \vdash P > P}{\it init}$$

$${\Gamma, A \vdash B \over \Gamma \vdash A \supset B}{{\supset}R} \qquad {\Gamma \vdash A \qquad \Gamma \vdash B > P \over \Gamma \vdash A \supset B > P}{{\supset}L}$$

$${\Gamma \vdash A(\alpha) \over \Gamma \vdash \forall x.A(x)}{{\forall}R^\alpha} \qquad {\Gamma \vdash A(t) > P \over \Gamma \vdash \forall x. A (x) > P}{{\forall}L}$$

... where $A$ and $B$ represent arbitrary propositions and $P$ represents an atomic proposition.

Relationship between the proof systems

We, roughly speaking, expect the two proof systems to prove the same things. One direction of this is easy:

Theorem 1 (Soundness of focusing) - If $\Gamma \vdash A$, then $\Gamma \Rightarrow A$, and if $\Gamma \vdash A > C$, then $\Gamma, A \Rightarrow C$.

Proof: Straightforward induction on focused proofs (+ weakening for the unfocused proofs).

The other direction is a bit trickier:

Theorem 2 (Completeness of focusing) - If $\Gamma \Rightarrow A$ then $\Gamma \vdash A$.

Before we discuss Theorem 2, the question is, why do we care about the focused proof system and its correspondence to the unfocused proof system at all? One answer is because it lets us prove the following theorem (restated from the original poster):

Corollary 1 - If $\Gamma \Rightarrow P$ then there exists $A \in \Gamma$ such that $\Gamma \vdash A > P$.

Proof: By Theorem 2 and the premise, $\Gamma \vdash P$. By case analysis, the last rule in this derivation must be $\it focus$, and the result follows immediately from the premises of that rule.

The completeness of focusing

There are a number of ways to prove the completeness of focusing; the approach I describe here is not the oldest and I don't claim it's the best, but it'll do; I'd welcome anyone else that wanted to elaborate other, possibly simpler, versions of this proof. Variations of this approach can be found in the following places:

Sadly-uncommented Twelf code: Robert J. Simmons, Weak Focusing. The Twelf Wiki.
The appendices of: Jason Reed and Frank Pfenning, Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic.
Mostly just hinted at: Frank Pfenning and Robert J. Simmons, Substructural Operational Semantics as Ordered Logic Programming. LICS 2009.
In a much more general form: Robert J. Simmons and Frank Pfenning, Weak Focusing for Ordered Linear Logic. CMU Tech Report.

The basic idea is to prove cut admissibility and identity expansion for the focused system only, and then use that to prove the critical "unfocused admissibility" lemmas, which show that any unfocused inference is valid over focused proofs. One reason that I like this presentation is that it shows how the completeness of focusing is a straightforward consequence of cut admissibility and identity expansion for the focused sequent calculus.

Theorem 3 is standard, and Theorem 4 is an equally important theorem that has been frequently neglected:

Part 1: Cut admissibility

Theorem 3 (Cut admissibility)

If $\Gamma \vdash A$ and $\Gamma \vdash A > C$, then $\Gamma \vdash C$.
If $\Gamma \vdash A$ and $\Gamma, A \vdash C$, then $\Gamma \vdash C$.
If $\Gamma \vdash A$ and $\Gamma, A \vdash B > C$, then $\Gamma \vdash B > C$.

Proof: These three statements are proved simultaneously by lexicographic induction: either the size of the principal formula $A$ gets smaller or the principal formula stays the same size while one of the provided derivations decrease in size (and the other stays the same).

Part 2: Identity expansion

Theorem 4 (Identity expansion) If there is a proof $$\Gamma \vdash A > P $$ $$\vdots$$ $$\Gamma \vdash P$$ that is parametric in $P$, then $\Gamma \vdash A$.

Proof: By induction on the structure of $A$.

Case $A = P'$. We are given a derivation parametric in $P$ that has an open leaf $\Gamma \vdash P' > P$ and that proves $\Gamma \vdash P$. By letting $P = P'$, we can show $\Gamma \vdash P' > P'$ by $\it init$, which gives us $\Gamma \vdash P'$, exactly what we needed to show.

Case $A = A \supset B$. We are given a derivation parametric in $P$ that has an open leaf $\Gamma \vdash A \supset B > P$ and that proves $\Gamma \vdash P$.

First, note that we can weaken this derivation to a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash A \supset B > P$ and that proves $\Gamma, A \vdash P$.

Second, note that the rule $\it focus$ allows us to create a derivation parametric in $Q$ that has an open leaf $\Gamma, A \vdash A > Q$ and that proves $\Gamma, A \vdash Q$. By the induction hypothesis, we can conclude $\Gamma, A \vdash A$.

These two derivations, together with rule ${\supset}L$, allow us to construct a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash B > P$ and that proves $\Gamma, A \vdash P$. By the induction hypothesis, we can conclude $\Gamma, A \vdash B$, and by rule ${\supset}R$, we can conclude $\Gamma \vdash A \supset B$.

Case $A = \forall x. A(x)$. (Omitted.)

This completes the identity expansion lemma which has, as a simple corollary, the identity theorem that for all $A$, $\Gamma, A \vdash A$ (we actually used this corollary in the second case).

Part 3: Unfocused admissibility

Now we can prove "unfocused admissibility" of all of the left rules:

Theorem 5 (Unfocused admissibility)

If $P \in \Gamma$, then $\Gamma \vdash P$.
If $(A \supset B) \in \Gamma$, $\Gamma \vdash A$, and $\Gamma, B \vdash C$, then $\Gamma \vdash C$.
If $(\forall x.A(x)) \in \Gamma$ and $\Gamma, A(t) \vdash C$, then $\Gamma \vdash C$.

The first statement we can prove immediately by ${\it init}$ followed by ${\it focus}$.

For the second statement, we use identity expansion to prove that $\Gamma, A \vdash A$. From this fact, the given fact that $A \supset B \in \Gamma$, and the ${\it focus}$ and ${{\supset}L}$ rules, it is possible to construct a derivation parametric in $P$ that has an open leaf $\Gamma, A \vdash B > P$ and that proves $\Gamma, A \vdash P$. Therefore, by identity expansion, $\Gamma, A \vdash B$. We were given that $\Gamma \vdash A$, so by cut admissibility, $\Gamma \vdash B$. We were also given that $\Gamma, B \vdash C$, so by cut admissibility, $\Gamma \vdash C$.

I'll omit again the proof of the third statement.

Part 4: Proving Theorem 2 by straightforward induction

Now that I have the unfocused admissibility theorems, proving the completeness of focusing is just a matter of straightforward induction over the unfocused derivations. Whenever we encounter a right rule we can use the induction hypothesis along with the corresponding rule in the focused sequent calculus. Whenever we encounter another rule we use the appropriate unfocused admissibility theorem.

Theorem 2 (Completeness of focusing) - If $\Gamma \Rightarrow A$ then $\Gamma \vdash A$.

Proof - By induction on the derivation $\Gamma \Rightarrow A$.

Case 1: $\mathcal D = {P \in \Gamma \over \Gamma \Rightarrow P}{\small \it init}$.

To show: $\Gamma \vdash P$.

Immediate from the assumption $P \in \Gamma$ (premise of ${\it init}$ and unfocused admissibility (part 1).

Case 2: $\mathcal D = {\Gamma, A \Rightarrow B \over \Gamma \Rightarrow A \supset B}{\small {\supset} R}$

To show: $\Gamma \vdash A \supset B$.

By the induction hypothesis, we have $\Gamma, A \vdash B$. Then, by rule ${\supset}R$, we have $\Gamma \vdash A \supset B$, which is what we needed to show.

Case 3: $\mathcal D = {(A \supset B) \in \Gamma \quad \Gamma \Rightarrow A \quad \Gamma, B \Rightarrow C \over \Gamma \Rightarrow C} {\small {\supset} L}$

To show: $\Gamma \vdash C$.

By the induction hypothesis, we have $\Gamma \vdash A$ and $\Gamma, B \vdash C$. Then the result follows from the fact that $(A \supset B) \in \Gamma$ and the unfocused admissibility lemma.

Case 4: (${\forall}R^\alpha$, omitted)

Case 5: (${\forall}L$, omitted)

Comment by Rob Simmons

2011-10-30T15:54:56Z

Beautiful question! Yes, you need to generalize the identity expansion property in an interesting and non-obvious way to handle positive propositions. Luckily, I have a paper on arXiv that describes how, which I plan to submit to a journal after a bit more revision: arxiv.org/abs/1109.6273

Comment by Rob Simmons

2011-07-16T17:19:58Z

Sorry: what I meant by "existentially" was precisely those variables that "arise naturally by a backward chaining step," which is why I said "existentially in the sense of Prolog."

Comment by Rob Simmons

2011-07-10T14:45:12Z

The way you wrote it, it looks like the rule and the relevant facts get removed from the context when you apply <tt>-> Forward</tt> (reading from the bottom up). This would certainly be non-deterministic, because starting from the sequent <tt>Q1, Q1 -> Q2, Q1 -> Q3 |- A</tt> only one of the two rules would be able to fire. Presumably that's not what you meant, though. I believe what you're asking to is related to the question of the semi-decidability of Prolog, which only holds if you use an un-Prolog-like breadth first search.

Comment by Rob Simmons

2011-05-30T04:23:29Z

What you can do is prove that, if you are trying to prove a sequent $\Gamma \vdash P$ where $\Gamma$ contains only Horn clauses and $P$ is atomic, the proof won't contain the ${\supset}R$ rule. This holds in both focused and unfocused systems. If you want, you can see the introduction of the ${\supset}R$ rule as akin to "generalizing the induction hypothesis." For the strategy I presented, you need a sound and complete logic, even though it contains some rules (${\supset}R$, ${\forall}R$) that you can prove you don't need for your uniform proofs.

Comment by Rob Simmons

2011-05-30T04:19:03Z

The restriction to Horn clauses is fine as far as it goes, but as you note, a sequent calculus with Horn clauses but without the ${\supset}R$ rule is incomplete - the sequent calculus system doesn't admit the identity property (becuase you can't prove $A \supset B \vdash A \supset B$) and the natural deduction system is unable to do $\eta$-expansion. So what you're claiming as the natural logic of Horn clauses is, I claim, not a well-formed logic. If you want to restrict propositions to the form $P \supset A$ with $P$ atomic, you can get a well-formed logic, but you still need ${\supset}R$

Comment by Rob Simmons

2011-05-29T03:27:30Z

In other words: there's already an accepted definition for a "logically permissible macro" - an admissible rule.

Comment by Rob Simmons

2011-05-29T03:26:27Z

As for the first BTW: certainly ${\supset}L$ is an admissible rule: just as all the unfocused rules were admissible in the focused system, natural deduction inference is admissible in a sequent calculus and vice versa. By "synthetic inference rules", I mean the observation that we can treat a valid formula as equivalent to an inference rule it gives rise to under focusing. And I wouldn't call it my notion: I got them from Chaudhuri who got them from Andreoli's bipoles, and the idea was around even before that in LF's notion of induction on canonical forms.

Comment by Rob Simmons

2011-05-28T14:27:37Z

While it may be a bit counterintuitive, you might find more people knowledgeable about this topic at the CSTheory StackExchange!