ImplicationLink
ImplicationLink or ImplicationScopeLink is used by OpenCog to express if...then... relations. The structure of an ImplicationLink is a set of predicates to be anded together (disjunct normal form), followed by one or more implicands. ImplicationLinks 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:
ImplicationLink P Q
where P is the implicant and Q is the implicand. Via the PLN implication instantiation rule, ImplicationLinks can also be thought of as graph re-write rules: if an instance of predicate P is observed, an instance of predicate Q is created. ImplicationLinks encode declarative knowledge, they are, in a sense, dual to BindLinks, which encode the same knowledge, but are procedural. See the page on atom relationships for a full list of such correspondences.
Definition
ImplicationLink <implicant-predicate> <implicand-predicate>
PLN Semantics
In PLN an ImplicationLink between 2 predicates is equivalent to an InheritanceLink between their satisfying sets. Formally
ImplicationLink <TV> P Q
is equivalent to
InheritanceLink <TV> SatisfyingSetLink P SatisfyingSetLink Q
Since InheritanceLink corresponds to a mixed extensional and intensional inheritance, then ImplicationLink is also mixed (this is often forgotten), that is ImplicationLink is also defined as:
OrLink <TV> ExtensionalImplicationLink P Q IntensionalImplicationLink P Q
Universal Conditioned Instantiation
One can directly use an ImplicationLink 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).
