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 atoms in the body is are 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