# Is forward chaining also a form of focusing?

Dear All

Lets restrict ourselfs to logical theories which consist only of formulas $P_1 \supset \quad ... \quad P_n \supset Q$, i.e. propositional horn clauses expressed with implication. Lets only assume a subset of minimal logic, no (->R), only (->L).

My starting point is the following very primitive calculus:

$${P \in \Gamma \over \Gamma \Rightarrow P}{(init)} \qquad {(P \supset A) \in \Gamma \qquad \Gamma \Rightarrow P \qquad \Gamma, A \Rightarrow Q \over \Gamma \Rightarrow Q}{({\supset}L)}$$

When we focus the (->L) that the head of A matches the goal Q, then we get backward chaining.

$${(P_1 \supset \quad ... \quad P_n \supset Q) \in \Gamma \qquad \Gamma \Rightarrow P_1 \quad ... \quad \Gamma \Rightarrow P_n \over \Gamma \Rightarrow Q}{({\supset}L \quad Back)}$$

Now I am experimenting with another variant of (->L). Instead of requiring that the head machtes the goal, I require that the atoms in the body are already given:

$${(P_1 \supset \quad ... \quad P_n \supset Q) \in \Gamma \qquad P_1 \in \Gamma \qquad ... \qquad P_n \in \Gamma \qquad \Gamma, Q \Rightarrow R \over \Gamma \Rightarrow R}{({\supset}L \quad Forward)}$$

Forward chaining has been characterized as deriving new facts from given facts. A couple of questions emerge:

* Is the forward chaining variant of the primitive calculus still complete?
* Is forward chaining also a from of focusing?
* Are there better ways to formulate forward chaining than with (->L Forward)?


Best Regards

P.S.: Question is inspired by the restated calculus in How establish conversion of cut-free proof into uniform proof?

P.S.S.: Here is an example of a backward chaining proof:

-------------- (init)
p, p -> q => p
-------------- (->L Back)
p, p -> q => q


And here is an example of a forward chaining proof:

----------------- (init)
p, p -> q, q => q
----------------- (->L Forward)
p, p -> q => q

-

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. –  Rob Simmons May 29 '11 at 3:26
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$ –  Rob Simmons May 30 '11 at 4:19