Is forward chaining also a form of focusing? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T13:10:21Z http://mathoverflow.net/feeds/question/66275 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/66275/is-forward-chaining-also-a-form-of-focusing Is forward chaining also a form of focusing? Countably Infinite 2011-05-28T12:59:55Z 2011-05-29T12:52:02Z <p>Dear All</p> <p>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).</p> <p>My starting point is the following very primitive calculus:</p> <p>$${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)}$$</p> <p>When we focus the (->L) that the head of A matches the goal Q, then we get backward chaining.</p> <p>$${(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)}$$</p> <p>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> <p>$${(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)}$$</p> <p>Forward chaining has been characterized as deriving new facts from given facts. A couple of questions emerge:</p> <pre><code>* 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 (-&gt;L Forward)? </code></pre> <p>Best Regards</p> <p>P.S.: Question is inspired by the restated calculus in <a href="http://mathoverflow.net/questions/65776/how-establish-conversion-of-cut-free-proof-into-uniform-proof/65854#65854" rel="nofollow">http://mathoverflow.net/questions/65776/how-establish-conversion-of-cut-free-proof-into-uniform-proof/65854#65854</a></p> <p>P.S.S.: Here is an example of a backward chaining proof:</p> <pre><code>-------------- (init) p, p -&gt; q =&gt; p -------------- (-&gt;L Back) p, p -&gt; q =&gt; q </code></pre> <p>And here is an example of a forward chaining proof:</p> <pre><code>----------------- (init) p, p -&gt; q, q =&gt; q ----------------- (-&gt;L Forward) p, p -&gt; q =&gt; q </code></pre> http://mathoverflow.net/questions/66275/is-forward-chaining-also-a-form-of-focusing/66280#66280 Answer by Rob Simmons for Is forward chaining also a form of focusing? Rob Simmons 2011-05-28T14:22:50Z 2011-05-28T14:51:12Z <p>So the short answer is "yes, the forward chaining calculus is complete." Is forward-chaining still a form of focusing? Well, yes, though giving a logical characterization to <em>saturation</em> in forward-chaining is currently a point of investigation.</p> <p>I think Kaustuv Chaudhuri was the first person to take Andreoli's observations about polarity and formally connect them to forward and backward chaining, though he did so in an unusual way (at least from my perspective, and, based on reading your question, from yours as well). In particular, Chaudhuri works from the perspective of the axioms-down (or <em>inverse method</em>) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in <em><a href="http://dx.doi.org/10.1007/s10817-007-9091-0" rel="nofollow">A Logical Characterization of Forward and Backward Chaining in the Inverse Method</a></em>, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, <em><a href="http://dtai.cs.kuleuven.be/projects/ALP/newsletter/may07/content/Articles/theoremproving/content.html" rel="nofollow">Polarities in Theorem Proving and Logic Programming</a></em>. Kaustuv might argue that the inverse method is one of the "better ways to formulate forward chaining than with (->L Forward)", though I don't exactly take this view (and don't want to put words in his mouth!)</p> <p>I wrote some notes about this some time ago in a blog post called <em><a href="http://requestforlogic.blogspot.com/2010/09/focusing-and-synthetic-rules.html" rel="nofollow">Focusing and Synthetic Rules</a></em> that tried to re-cast some of Chaudhuri's observations from the perspective of bottom-up proof search. Also, in the (woefully-un-commented) Twelf Wiki <a href="http://twelf.plparty.org/wiki/Weak_focusing" rel="nofollow">article</a> presenting a variant of the completeness-of-focusing proof that I sketched in the previous answer, I actually had some fun using the computational content of the completeness-of-focusing argument to actually <a href="http://twelf.plparty.org/wiki/Weak_focusing#Forward_and_backward_chaining" rel="nofollow">transform proofs into forward-chaining form and backward-chaining form</a>. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.</p>