Dear All

Lets restrict ourselfs to logical theories which consist
only of formulas P1 -> .. Pn -> 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 G               P -> A in G  G => P  G, A => Q  
    ------- (init)       ------------------------------ (->L)
    G => P                          G => Q

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

    P1 -> .. Pn -> Q in G  G => P1  ... G => Pn
    -------------------------------------------- (->L Backward)
                      G => Q

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

    P1 -> .. Pn -> Q in G    P1 in G ... Pn in G     G, Q => R
    --------------------------------------------------------- (->L Forward)
                      G => R

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 http://mathoverflow.net/questions/65776/how-establish-conversion-of-cut-free-proof-into-uniform-proof/65854#65854

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