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