# Inference

## Forward and Backward Chaining

An inference problem can be formulated as follows:
1. There is a set of sentences given as true, the hypotheses
2. There is a sentence which it is desired to prove, call this the conclusion
3. There are rules of inferecne that permit the deduction of additional sentences from given ones.
4. Use the given rulkes of inference to deduce the conclusion from the hypotheses
For concreteness call the set of given sentences the Knowledge base KB, the conclusion g. Then we want to show KB |- g where |- stands for the use of our given inference procedure. This might for example be the generalised modus ponens of page 269 of AIMA.

In trying to construct a proof we can describe two apporaches. These are not exhaustive but they embody the two major "local " strategies.

Forward chaining
Given the knowledge base KB we can find an inference rule
Hypotheses
-----------
Conclusion
whose hypotheses unify with sentences in KB, we can then add the conclusion to the knowledge base (after making the substitutions required to math the hypotheses to the sentences of KB). This gives us a new KB in which more in known and we can repeat the process until g appears as the conclusion of one of these steps. We are then done.
Backward chaining
This time we start with g and look for an inference rule
Hypotheses
-----------
Conclusion
such that the conclusion can be unified with g. It then is enough to proof the hypotheses of this rule.

Note that Forward chaining can produce many irrelevant conclusions before arriving at a proof. Whereas backward chaining may pursue a misleading line of proof without some control.

## Resolution

Resolution is a simple proof rule that is a complete inference procedure, at least in the sense that if the sentnces in the hypothesis lead to a contradiction resolution will determine that fact.

For literals pi and qi where pj and ~qk unify with unifier s

p1 \/ p2\/ ...\/pj\/ ...\/ pm
q1\/...qk\/... qn
-----------------------------------------------
subst(s, (p1\/p2 .. pj-1\/pj+1\/..\/pm\/q1\/..qk-1\/qk+1..\/qn))
Note that resolution can be used in either direction.