* Natural deduction* methods perform deduction in a manner similar to
reasoning used by humans, e.g. in proving mathematical theorems.

* Forward chaining* and * backward chaining* are natural deduction
methods. These are similar to the algorithms described earlier for
propositional logic, with
extensions to handle variable bindings and unification.

Backward chaining by itself is not complete, since it only handles
* Horn clauses* (clauses that have at most one positive literal).
Not all clauses are Horn; for example, ``Every person is male or female''
becomes *¬ Person(x) &or Male(x) &or Female(x)* which has two
positive literals. Such clauses do not support backchaining.

* Splitting* can be used with backchaining to make it complete.
Splitting makes assumptions (e.g. ``Assume *x* is Male'') and attempts to
prove the theorem for each case.