Support meta-rule in the URE

[opencog]

Support meta-rule in the URE

[ngeiswei]

Meta-rules are almost completely supported by the URE, however building inference trees with them is trickier than I thought so what the forward and backward chainers are doing for now is merely turn them into regular rules, see https://github.com/opencog/atomspace/blob/master/opencog/rule-engine/backwardchainer/BackwardChainer.cc#L133 https://github.com/opencog/atomspace/blob/master/opencog/rule-engine/forwardchainer/ForwardChainer.cc#L130, then build inference trees with those regular rules.

The problem comes when going backward because the inference tree looses the process that led to turning the meta-rules into regular rules, and thus looses the premises of the meta-rules!

This makes some forms of backward chaining impossible, for instance:

Given the axioms

(Implication (stv 1 1)
  (Predicate "P")
  (Predicate "Q")

(Implication (stv 1 1)
  (Predicate "Q")
  (Predicate "R")

(Evaluation (stv 1 1)
  (Predicate "P")
  (Concept "a"))

You want to prove R(a). You have at least 2 ways to do that

1. Prove (Implication (Predicate "P") (Predicate "R")), i.e. P->R, using deduction https://github.com/opencog/opencog/blob/master/opencog/pln/rules/term/deduction.scm, then use conditional instantiation https://github.com/opencog/opencog/blob/master/opencog/pln/meta-rules/predicate/conditional-full-instantiation.scm, to obtain R(a) from P(a).
2. Or, chain 2 conditional instantiations, the first one to obtain Q(a) from P(a), and the second one to obtain R(a) from Q(a).

Currently the backward chainer will only be able to prove R(a) the second way, not the first way, because in the first way, by the time the inference is being built, the knowledge of P->R hasn't been built yet, thus the conditional instantiation meta-rule cannot be converted into a regular rule.

After thinking more deeply about it, I've concluded that to solve that we need to have a UnifyLink of some sort to express the notion of unification in Atomese, which is currently only exposed to the C++ code https://github.com/opencog/atomspace/blob/master/opencog/unify/Unify.h but that's pretty foggy at that point, probably the more specialized notion of unification between inference tree premise (or conclusion) with rule conclusion (or rule premise) is enough...

[linas]

Looks reasonable to me.

One theoretical comment. We've long said that ImplcationLinks (ImplicationSvopeLinks) encode "declarative knowledge", while BindLinks are "just like Implication links, except that they're proceedural" So I think it is kind of funny that we are finally creating a "meta-rule" that can convert implication-links to bind-links.

The full table is at the bottom of the page http://wiki.opencog.org/w/Atom_relationships -- perhaps you want to have a meta-rule for each and every one of these?

[linas]

However, this also raises a different question: Perhaps BindLinks and ImplicationScopeLibnks should actually be exactly the same thing? Why do we need to have two "almost the same" links ... maybe just having one would be simpler (in the long run)?

Right now, BindLink has a big complicated init sequence, but maybe we should change it to not do any init at all, until the first time that the pattern matcher is invoked on it? That way, BindLink and ImplicationScope really could be the same type...

[bgoertzel]

ImplicationScopeLink has truth value semantics based on conditional
probability, BindLink does not necessarily do so ...

On Wed, Nov 9, 2016 at 12:05 AM, Linas Vepštas [email protected]
wrote:

However, this also raises a different question: Perhaps BindLinks and
ImplicationScopeLibnks should actually be exactly the same thing? Why do we
need to have two "almost the same" links ... maybe just having one would be
simpler (in the long run)?

Right now, BindLink has a big complicated init sequence, but maybe we
should change it to not do any init at all, until the first time that the
pattern matcher is invoked on it? That way, BindLink and ImplicationScope
really could be the same type...

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
https://github.com/opencog/atomspace/issues/986#issuecomment-259299266,
or mute the thread
https://github.com/notifications/unsubscribe-auth/AFolXL9bsPVxNrdOxKu2693Qh0YPXfKIks5q8Q5fgaJpZM4KsO5A
.

Ben Goertzel, PhD
http://goertzel.org

“I tell my students, when you go to these meetings, see what direction
everyone is headed, so you can go in the opposite direction. Don’t polish
the brass on the bandwagon.” – V. S. Ramachandran

[amebel]

Is meta-rule a means of expanding a macro-rule, so as to make it visible to ure-bc?

[ngeiswei]

@amebel not exactly, although it could. A meta-rule is merely a rule that produces a rule. The URE wouldn't necessarily need to support it, it could just handle that in 2 steps (although it would at least need to add the produced rule in the rule-base) but I feel it's probably better to do the 2 step on the fly. I haven't started coding so I'll see.

[ngeiswei]

@linas yes I completely see the irony and it made me think a bit, as Ben said I think the ImplicationLink is a specialized BindLink with predefined TV formula on the rewriting term.

[linas]

OK. Its OK to leave this as is, but just keep that question active in the back of your mind for the next few years, as it may need to be revisited.

[ngeiswei]

A good example requiring full meta-rule support in the backward chainer can be found here https://github.com/opencog/opencog/tree/master/examples/pln/good-songs

[ngeiswei]

Another example is BackwardChainerUTest::test_induction() that would be re-enabled once meta-rule is supported.

[ngeiswei]

A propotype written by @rTreutlein waiting to be merge can be found in that branch

https://github.com/opencog/ure/tree/rTreutlein-MetaRuleSupport