The process of working backwards from a given goal. Used in: Theorem Prover Inference Methods Selective Linear Definite Clause Resolution