ImplicationScopeLink
An ImplicationScopeLink is used by OpenCog to express if...then... relations. The structure of an ImplicationScopeLink is a set of predicates to be anded together (disjunct normal form), followed by one or more implicands. ImplicationScopeLinks may contain variables that are bound for the scope of the implication. They may be thought of as expressions in first-order logic; i.e. VariableNodes may only be grounded by nodes, not links; grounding by links is discussed below.
ImplicationLinks encode basic logical implication P->Q, i.e. if P then Q as:
Definition
ImplicationScopeLink <variables> <implicant-predicate-body> <implicand-predicate-body>
which is equivalent to
ImplicationLink LambdaLink <variables> <implicant-predicate-body> LambdaLink <variables> <implicand-predicate-body>
Where the LambdaLinks are used as predicate constructors.
Theory
The ArrowLink is the Curry–Howard correspondent to the ImplicationLink. That is, the ImplicationLink is designed to work with predicates, whereas the ArrowLink is designed to work with atoms in general. More narrowly, the ArrowLink is a type constructor, used to define the function type. See also currying.
Example
Consider the English language sentence "Fido is a dog". A dependency parse of this sentence would result in the dependency graph "_subj(be,Fido) _obj(be,dog)". Suppose that, given this dependency parse, we want to conclude that "isa(dog,Fido)". In FrameNet notion, this would be:
# IF _subj(be,$var0) ^ _obj(be,$var1) THEN isa($var1, $var0)
When written out in OpenCog format, this becomes an ImplicationScopeLink
ImplicationScopeLink VariableList TypedVariableLink VariableNode "$var0" TypeNode "ConceptNode" TypedVariableLink VariableNode "$var1" TypeNode "ConceptNode" AndLink EvaluationLink PredicateNode "_subj" ListLink ConceptNode "be" VariableNode "$var0" EvaluationLink PredicateNode "_obj" ListLink ConceptNode "be" VariableNode "$var1" EvaluationLink PredicateNode "isa" ListLink VariableNode "$var1" VariableNode "$var0"
Note that each triple was expressed in terms of EvaluationLinks. A perl script that will convert the first, short form, into the second, can be found in the source tree, at opencog/nlp/chatbot-old/triples/rules-to-implications.pl. Additional documentation can be found in opencog/nlp/chatbot-old/triples/README.
PLN Semantics
As stated above
ImplicationScopeLink <variables> <implicant-predicate-body> <implicand-predicate-body>
is equivalent to
ImplicationLink LambdaLink <variables> <implicant-predicate-body> LambdaLink <variables> <implicand-predicate-body>
By virtue of the ImplicationLink being an extension/intensional mixed implication, it is also equivalent to
OrLink ExtensionalImplicationScopeLink <variables> <implicant-predicate-body> <implicand-predicate-body> IntensionalImplicationScopeLink <variables> <implicant-predicate-body> <implicand-predicate-body>
Universal Conditioned Instantiation
One can directly use an ImplicationScopeLink a universal quantifier with a precondition (the implicant). The implicant indicates the domain of the quantifier, and the TV on the ImplicationLink indicates the degree of its universality within that domain.
Implication instantiation rules can be used to generate implicand instances so that the implicant instances are true (at least to some extend). The TV of the implicand is by default obtained via the PLN implication instantiation rule (TODO: create a wikipage for that rule).
