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?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
