Lets restrict ourselfs to logical theories which consist only of formulas P1 -> .$P_1 \supset \quad .Pn -> Q.. \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).

P 
$${P \in G               P -> \Gamma \over \Gamma \Rightarrow P}{(init)}{(P \supset A) \in G  G => \Gamma \qquad \Gamma \Rightarrow P G, \qquad \Gamma, A => Q  ------- (init)       ------------------------------ (->L)G => P                          G => \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.
P1 -> .
$${(P_1 \supset \quad .Pn -> .. \quad P_n \supset Q) \in G  G => P1  \Gamma \qquad \Gamma \Rightarrow P_1 \quad ... G => Pn-------------------------------------------- (->L Backward)                  G => Q\quad \Gamma \Rightarrow P_n \over \Gamma \Rightarrow Q}{({\supset}L \quad Back)}$$
P1 -> .
$${(P_1 \supset \quad .Pn -> .. \quad P_n \supset Q) \in G    P1 \Gamma \qquad P_1 \in G \Gamma \qquad ... Pn \qquad P_n \in G     G, \Gamma \qquad \Gamma, Q => R--------------------------------------------------------- (->L Forward)                  G => \Rightarrow R \over \Gamma \Rightarrow R}{({\supset}L \quad Forward)}$$
* Is the forward chaining variant of the primitive calculus still complete?* Are there better ways to formulate forward chaining than with (->L ->L Forward)?
        

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

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 


P1 -> A .. Pn -> Q in G    P P1 in G ... Pn in G     G, A Q => Q
R
---------------------------------- -------------------------------------------------------- (->L Forward)
                  G => Q
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


        

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

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? What calculi have been developed for
• Are there better ways to formulate forward chaining .than with (->L Forward)?

Best Regards

P.S.: Question is inspired by the restate 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

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

Is forward chaining also a from of focusing? What calculi have been developed for forward chaining.

Best Regards

P.S.: Question is inspired by the restate 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