This is sometimes called forward reasoning or forward chaining . But inference rules can also be used in the opposite direction to determine under which conditions a given goal can be derived. This is called backward reasoning or backward chaining . Note that the condition is sufficient , but not necessary , as there are of course other ways to verify that John satsifies the CSE-113 prerequisites. Programming in Logic Predicate logic formulas can be used to write programs in a programming language called Prolog .
Rules are universally quantified implications of a certain form.
The input to a logic program is called a Goal , an existentially quantified atomic formula, usually with variables. Ormonde to the initial goal. The result of a computation with a logic program is a proof that the goal is a logical consequence of the facts and rules. Here is a proof corresponding to the last computation. When executing a logic program one has to explore all possible backward chains.