 A problem being presented to an automated reasoning program consists of two main items, namely a statement expressing the particular question being asked called the problem’s conclusion, and a collection of statements expressing all the relevant information available to the program—the problem’s assumptions. Solving a problem means proving the conclusion from the given assumptions by the systematic application of rules of deduction embedded within the reasoning program. The problem solving process ends when one such proof is found, when the program is able to detect the non-existence of a proof, or when it simply runs out of resources.