PLN Forward Chainer
I think this is all that's left not working in FC:
- SimSubstRule (may require special code, but nothing too complicated)
- CrispTheoremRule (replaceable with ModusPonensRule; it makes the current BC faster due to tacky heuristics, but that's not relevant to FC)
- CustomCrispUnificationRule only works for some cases. Definitely used in some of our demos)
The second version of the forward chainer worked like this: In each step, try every Composer, and try using every Generator to produce the arguments to it. It had three major problems:
1) Looking up Atoms gets very slow after a few hundred have been added. I'm not sure how much this is because of the indexes, or how much it is because of the unify methods (used to check if each Atom matches). 2) The chainer has a combinatorial explosion. Most significantly, it keeps making lots of AND/OR expressions, and then combining those with more AND/OR expressions, etc. This might be fixable by the following change: the FC doesn't produce such Links, it only evaluates them (if they are in an existing ImplicationLink). That would be more like a "normal" forward chainer. 3) It couldn't handle ForAll expressions that fill in each other's variables.
The third version is a lot better. The Rules are divided into "deduction-related Rules" and "evaluation-related Rules". Rules like Deduction/ModusPonens/Inversion are the deduction-related Rules. The evaluation-related Rules evaluate things like AND/OR/NOT expressions.
In each inference step, the FC tries every deduction-related Rule. It uses the backward chainer to find the inputs to that Rule. For this purpose, the BC is set up to only use evaluation Rules. This design is similar to classical logic forward chainers. An example step would be Modus Ponens, say you know (A&B&C => D) as well as A, B and C. The BC would use LookupRule to find the ImplicationLink, and then use SimpleANDRule to find the AndLink (using LookupRule to find them. It will also try to use ForAll expressions to produce any of the Atoms.
It turns out the backchainer is efficient if you only use evaluation Rules, because there aren't many ways to produce each thing, and it can only chain a few levels. This design also ensures that AND/OR/NOT expressions are only (and always) produced when necessary.
There is a case that FC simply can't handle, not as it's currently conceived. A result can be produced using say ModusPonens on a single ImplicationLink, where the Implication and the premise are produced from ForAll expressions. Maybe each of the ForAll expressions will have constants in places where the other has Variables. If not, then there will still be Variables left unfilled, which will likely require special support. The BC can avoid this problem if you *specify* the details (values) in the BC target.
i.e. as a fake example
ForAll $A $B: foo($A $B) ForAll $C : foo(apple $C) => gack(apple $C)
If you use ModusPonens in FC it will produce gack(apple $C). If you used BC to ask for gack(apple cat) there'd be no Variable left; FC can't produce that from these axioms without a suitable process to choose the Atom (even though it's a valid inference).
There is another more complex case that the current forward chainer can't handle. Where you have two or more ImplicationLinks used together (via Deduction or ModusPonens), and they are produced from ForAllLinks (or other generalisation links), and their premises are too. You're trying to prove a complex fact, and each ImplicationLink adds extra details (i.e. Variables are being filled in as you go along, because some of the ImplicationLinks are more specific in some ways).
I suspect this is used in several of the current tests/demos, including for fetch and word-object association (i.e. problems that a near-future OpenCog AI should be able to solve).
I've thought of various ways to solve these problems, possibly the most promising one involves using general conditional proof a la chapter 12 of http://faculty.washington.edu/smcohen/120/LectureNotes.htm (which btw is an excellent resource on subtle issues in logical proofs).