u using the rules from the goal we get some more internal “subgoals”, u to prove the subgoals, we get other subgoals u until we can prove them with the facts. u Example of backward chaining mechanism: Prolog - Flex