Backward inference

Backward inference refers to a mode of inference in which rules do not fire until Cyc is asked a query. If a rule is relevant to the query and transformation is allowed, the rule can be considered and might participate in a proof of the answer. This is in contrast to forward inference, in which a forward rule is triggered when a new assertion is added to Cyc that matches a literal on the rule’s antecedent.

“Backward” is one of the possible values for direction that an assertion may have. If an assertion is :backward, it may participate in backward inference only.

Backward inference example: If the user asks “What things are green?”:

(colorOfObject ?X GreenColor)

the inference engine could choose to use a rule in the KB that says “All leaves are green”:

RULE 1:

(implies 
    (isa ?LEAF Leaf)
    (colorOfObject ?LEAF GreenColor))

If Cyc backchains on this rule, it would transform the problem into:

(isa ?X Leaf)

Then if it can find something that is a leaf (like #$Leaf0037) from:

(isa Leaf0037 Leaf)

thus satisfying the antecedent of the rule, it uses removal and then bubbles up the binding #$Leaf0037 for ?X to prove:

(colorOfObject Leaf0037 GreenColor)

In backward inference, Cyc wouldn’t bother finding something to satisfy the antecedent of RULE 1 until it is asked a query that in part matches the consequent of RULE 1.