Applying a rule forwards or backwards is in fact a technique of using Natural Deduction rules in Pandora.

Generally, in order to apply a rule forwards in Pandora, you will click on an empty line in your proof at first, and then choose the rule to apply; where in order to apply a rule backwards, you will click on a goal in your proof at first, and then choose the rule to apply.

After applying a rule forwards, you will have a new formula which is not a goal of your proof. Usually a rule should be applied forwards only when you know the new formula derived will be helpful in proving the existing goal(s) of your proof.

There are three cases after applying a rule (except the Lemma Rule) backwards:

• In the first case (eg. Arrow Elimination), you will have a new formula which becomes a new goal consecutively before the old goal in your proof. Meanwhile, your old goal will be assumed to be derived by using the rule with the new goal (and possibly with other existing formulae which are in scope of the old goal). This is because if you can manage to prove the new goal, then the old goal can definitely be derived by using the rule forwards with the new goal (and possibly with other existing formulae which are in scope of the old goal).
• In the second case (eg. Arrow Introduction), you will be awarded an additional formula (known as the Assumption) at the top of a box and have a new formula (known as the Conclusion/goal) at the bottom of the box. Meanwhile, the old goal will be assumed to be derived from the box (by the assumption and the conclusion). In this case, usually the assumption will play an important part while proving the new goal in the box.
• The last case (eg. Or Elimination) is similar to the second case, except that you will have two boxes with different assumptions and a same goal.

In a word, a rule should be applied backwards if you want to replace your current goal in the proof with a new goal, which might be easier to prove, and/or if you want some additional "givens"(assumptions) to help in proving the goal. Using a rule backwards sometimes is a very powerful technique, especially when you are stuck in proving a goal.

"Proving backwards is a common stratege -- Instead of trying to show the goal from the data directly, you may also try to show the situation in which the goal is true, and then have the goal."

You can find out the directions in which a rule can be applied from the Rules Table of this page.