# 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:

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