Skip to main content
MathOverflow

Return to Revisions

3 of 7
edited body
user avatar
user avatar

Is forward chaining also a form of focusing?

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:

P -> A in G     P in G     G, A => Q
---------------------------------- (->L Forward)
            G => Q

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
Countably Infinite