1
$\begingroup$

Dear All

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

My starting point is the following very primitive calculus:

$${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)}$$

When we focus the (->L) that the head of A matches the goal Q, then we get backward chaining.

$${(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)}$$

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_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)}$$

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
Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
8
  • $\begingroup$ While it may be a bit counterintuitive, you might find more people knowledgeable about this topic at the CSTheory StackExchange! $\endgroup$
    – Rob Simmons
    Commented May 28, 2011 at 14:27
  • $\begingroup$ BTW: If the inverse method refers to Maslov, then it is also a kind of backward chaining, the only difference is that Maslov did not work with two sided sequents, but with sequents that contained T and F formulas. But it is a backward chaining on a higher level, on viewing how to apply the whole deductive system. But any deductive system can be applied both backward and forward. But here we try to identify backward and forward chaining inside a given deductive system. $\endgroup$
    – Countably Infinite
    Commented May 28, 2011 at 18:11
  • $\begingroup$ As for the first BTW: certainly ${\supset}L$ is an admissible rule: just as all the unfocused rules were admissible in the focused system, natural deduction inference is admissible in a sequent calculus and vice versa. By "synthetic inference rules", I mean the observation that we can treat a valid formula as equivalent to an inference rule it gives rise to under focusing. And I wouldn't call it my notion: I got them from Chaudhuri who got them from Andreoli's bipoles, and the idea was around even before that in LF's notion of induction on canonical forms. $\endgroup$
    – Rob Simmons
    Commented May 29, 2011 at 3:26
  • $\begingroup$ In other words: there's already an accepted definition for a "logically permissible macro" - an admissible rule. $\endgroup$
    – Rob Simmons
    Commented May 29, 2011 at 3:27
  • $\begingroup$ The restriction to Horn clauses is fine as far as it goes, but as you note, a sequent calculus with Horn clauses but without the ${\supset}R$ rule is incomplete - the sequent calculus system doesn't admit the identity property (becuase you can't prove $A \supset B \vdash A \supset B$) and the natural deduction system is unable to do $\eta$-expansion. So what you're claiming as the natural logic of Horn clauses is, I claim, not a well-formed logic. If you want to restrict propositions to the form $P \supset A$ with $P$ atomic, you can get a well-formed logic, but you still need ${\supset}R$ $\endgroup$
    – Rob Simmons
    Commented May 30, 2011 at 4:19

You must log in to answer this question.