Skip to main content
Post Deleted by Rob Simmons
added 209 characters in body
Source Link

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 saturation in forward-chaining is currently a point of investigation.

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 inverse method) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in A Logical Characterization of Forward and Backward Chaining in the Inverse Method, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, Polarities in Theorem Proving and Logic Programming. 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!)

I wrote some notes about this some time ago in a blog post called Focusing and Synthetic Rules 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 article 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 transform proofs into forward-chaining form and backward-chaining form. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.

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 saturation in forward-chaining is currently a point of investigation.

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 inverse method) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in A Logical Characterization of Forward and Backward Chaining in the Inverse Method, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, Polarities in Theorem Proving and Logic Programming.

I wrote some notes about this some time ago in a blog post called Focusing and Synthetic Rules 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 article 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 transform proofs into forward-chaining form and backward-chaining form. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.

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 saturation in forward-chaining is currently a point of investigation.

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 inverse method) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in A Logical Characterization of Forward and Backward Chaining in the Inverse Method, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, Polarities in Theorem Proving and Logic Programming. 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!)

I wrote some notes about this some time ago in a blog post called Focusing and Synthetic Rules 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 article 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 transform proofs into forward-chaining form and backward-chaining form. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.

Source Link

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 saturation in forward-chaining is currently a point of investigation.

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 inverse method) search for proofs rather than the perspective of build-the-tree-based-on-the-current-goals proof search. This is detailed in A Logical Characterization of Forward and Backward Chaining in the Inverse Method, and a simplified discussion can be found in Chaudhuri's March 2007 ALP newsletter article, Polarities in Theorem Proving and Logic Programming.

I wrote some notes about this some time ago in a blog post called Focusing and Synthetic Rules 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 article 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 transform proofs into forward-chaining form and backward-chaining form. The commentary at the end, unlike the completeness-of-focusing proof, does include some explanatory text.