Though the Natural Deduction rules are natural, they are still syntactic. A computer could do a natural deduction proof by applying suitable rules without knowing about the 'meaning' of the logic connectives (eg. The Pandora Tutor in the Tutorial).

Once you have put the assumptions at the top of a proof and the conclusion at the bottom, what do you do next? You might be able to use some automatic steps. Introduction rules produce conclusions so usually they are used when filling in a proof from the bottom upwards; where elimination rules work on the data and so they are usually used when filling in a proof from the top downwards. In Pandora, there are two ways of applying a rule - Forwards and Backwards. If you know what you do next will make progresses to the proof, then you may apply the rules straight away (forwards) on the data. Otherwise, it is worth you trying out the rules backwards with the conclusion/goal.

There are many useful tactics which you will discover for yourself. The following is a subset of the tactics (that are used by the Pandora Tutor):

• Work on the goal
  If you are sure that what you do next will make progresses to the proof, you may apply the rules on the data forwards straight away. If not, it might be a good idea to check the principle connective of the current goal. For example, if the current goal is:
  • A → B: then try to use Arrow Introduction(backwards). After doing that, you will have B as your new goal and what you do next is to prove B from A and/or other existing data (formulae that are in scope of B).
  • ¬P: then try to use Not Introduction(backwards). Then what you do next is to find a contradiction (that is, to prove Bottom/Falsity) from the existing data by assuming P.
  • a conjunction or disjunction: then use And Introduction(backwards) or Or Introduction(backwards). However, while using Or Introduction(backwards), you have to decide which subformula of the disjunction should become the new goal. Oftenly only one side of the disjunction is provable.
  • A ↔ B: then try to use IFF Introduction(backwards) or IFF Introduction-derived(backwards).
  • with quantifier ∀ or ∃: if you cannot derive them by using the rules forwards on the existing data, then you may have to use the corresponding introduction rule backwards on the goal. Using There Exists Introduction(backwards) sometimes is quite hard because you have to select a suitable term for the variable in the goal.
• Work on the data
  Sometimes, if you have no idea what to do with the goal, you might be able to temporarily ignore the goal and work on the data only (using rules forwards), hoping you can derive something new and useful to the proof. For example:
  • And Elimination(forwards): If there is an conjunction in your proof, then you may use And Elimination to extract its sub-formulae. Maybe they can help in proving the goal.
  • Arrow Elimination(forwards): If there exist an implication A → B and a formula A in your proof, then you may use Arrow Elimination(forwards) with them to derive D, which might be useful later on.
  • Not Elimination(forwards)/Bottom Introduction(forwards) with Bottom Elimination(forwards): If there exist P and ~P in your proof, the best next-step will be using Not Elimination(forwards) or Bottom Introduction(forwards) (in fact, they are the same) to derive Bottom/Falsity, and then use Bottom Elimination(forwards) to derive the goal.
• Work on both the data and the goal
  These tactics require you to check both the data and the current goal. Sometimes if you find the current goal is hard to prove, you might be able to use some rules backwards with the data and the current goal to get a new goal, which might be easier to prove. For example:
  • → as 'if': If there is an implication D → C and the conclusion is C then try to use Arrow Elimination(backwards) to derive D as a new goal, and then try to show D. D → C can be read as C if D, from which the tactic gets its name.
  • Make use of negated-formula: If the conclusion is Bottom/Falsity and there is a negated-formula say ¬P available, then you could use Not Elimination(backwards) to change the current goal from Bottom/Falsity to P.
  • Combined V rules: The Or Introduction and Or Elimination often go together. If the goal is a disjunction, say C V D, and there is also a disjunction, say A V B in scope of the goal, you may first use Or Elimination(backwards) and then use Or Introduction. The Or Elimination rule will force two subproofs, one using A and one using B, and perhaps in one you can prove C and in the other D. In both cases the Or Introduction rule will yield C V D, as you required..
  • Bottom Elimination(backwards) anywhere: If you cannot see what to do next perhaps you can use Bottom Elimination(backwards) to derive Bottom/Falsity as your new goal. This often happens in some branches of a Or Elimination box.
• Other tactics
  There are some other rules that you may want to try if all else fails,
  • Law of Excluded Middle: If you are really stuck, you may introduce a theorem of the form P V ¬P and immediately use Or Elimination. However, to select a suitable P is sometimes quite hard.
  • PC: Instead of trying the Law of Excluded Middle, you may also want to try the PC(Proof by Contradiction) rule. However, if all else does not fail then do not use PC, as the negated assumptions it introduces often make the proof more difficult to read.
  
  Practically, Lemmas are used in some large scale proofs. Sometimes, a large proof can best be tackled by breaking it down into smaller steps. For example, if your problem is to show Data |- Conclusion then maybe you could show Data |- Lemma and then make use of the Lemma to show Data + Lemma |- Conclusion.