Open rTreutlein opened 5 years ago
I can see 3 ways
deduction-implication-scope-rule
as you suggestdeduction-implication-rule
can then work).deduction-implication-rule
to implicitly add missing variables when necessary.I don't know which way is better, but I suppose it doesn't hurt to offer scoped variations of deduction rules, experiment and see, etc.
OK, I remember why the deduction rule is non-scoped, that is because the formula requires the probability of the predicates, and a mere ImplicationScope
doesn't give that. However the correct thing to do is to add A, B and C as premises of the deduction rule, do you see what I mean?
I am going to try to implement deduction-impliction-scope-rule
with A,B and C as premises.
Please excuse my random remarks. The bug report looks very valid. The intermdiate forms look broken:
(ImplicationLink (stv 1 1)
(LambdaLink
(VariableList (VariableNode "$A") (VariableNode "$B"))
stuff)
(LambdaLink
(VariableList (VariableNode "$A") (VariableNode "$B"))
other-stuff)
)
There's nothing to connect the variables in the first clause to the variables in the second clause, except for an accidental name-collision. The above is the same as
(ImplicationLink (stv 1 1)
(LambdaLink
(VariableList (VariableNode "$A") (VariableNode "$B"))
stuff)
(LambdaLink
(VariableList (VariableNode "$X") (VariableNode "$Y"))
other-stuff)
)
and who's to say that X and Y should be A and B? How could one ever know?
I think the rule that you want would be
(Bind
(TypedVariable (Variable "$P") (Type 'PredicateNode))
(ImplicationScopeLink
(VariableList (VariableNode "$A") (VariableNode "$B"))
(EvaluationLink
(PredicateNode "does")
(ListLink (VariableNode "$A") (VariableNode "$B")))
(EvaluationLink
(Variable "$P")
(VariableNode "$B")))
(ImplicationScopeLink
(VariableList (VariableNode "$X"))
(EvaluationLink
(Variable "$P")
(VariableNode "$X"))
(EvaluationLink
(PredicateNode "willbedone")
(VariableNode "$X")))
Note that $A, $B and $X are unrelated (and bound) while $P will be pattern matched to (PredicateNode "isbeingdone")
Now I really do not understand the internals of the backward-chainer, but above seems like a reasonable kind of rule ... yes?
The scoped implication deduction is reasonable, I agree, just want to point out that the non-scope implication rule using lambdas is also reasonable.
(ImplicationLink (stv 1 1) (LambdaLink (VariableList (VariableNode "$A") (VariableNode "$B")) stuff) (LambdaLink (VariableList (VariableNode "$X") (VariableNode "$Y")) other-stuff) )
and who's to say that X and Y should be A and B? How could one ever know?
I think what connects A and B with X and Y is the order. But i agree that this is a very flimsy representation.
I have been thinking about ImplicationScope to Implication conversion (and the reverse) and found some issues.
Let's say we have:
It seems reasonable to think that we can infer the following:
But atm this does not work. Let's try to do it and see where we fail. First we will have to use the
implication-scope-to-implication-rule
as thededuction-implication-rule
we want to use only works on normal ImplicationLinks. This results in the following:And here we can see the issue. Namely that the LambdaLink wrapping the "isbeingdone" Predicate has 2 variables in one case and 1 in the other which stops the
decuction-implication-rule
from doing anything. And if I understand this correctly can't change theimplication-scope-to-implication-rule
to just drop the extra Variable as that would break the equivalence between ImplicationScopeLink and the ImplicationLink. So i think the correct solution would be to create adecuction-implication-scope-rule
that can handle ImplicationScopeLinks by doing unification to get the mappings between variables and then using alpha-conversion to get 2 Links where the Variables Names line up correctly and then doing normal deduction.