In teaching students about proofs and their development, it helps to be able to demonstrate principles and strategies for developing proofs. Here are several useful ones that appear in A Logical Approach. They are perhaps obvious to the mature mathematician or computer scientist. However, to students they are not. Mathematicians and computer scientists have, in general, not discussed such principles and strategies, and that is one reason students have previously had trouble developing proofs.

• Heuristic. To prove P == Q, transform P == Q to a known theorem, transform P to Q, or transform Q to P.
  
  
• Heuristic. The operators that appear in an expression and the shape of its subexpressions focus the choice of theorems to be used in manipulating it. Therefore, in developing the next step of a proof, identify applicable theorems by matching theorems with the structure of the subexpressions of the current expression.
  
  
• Heuristic of Operator Elimination (fold/unfold). To prove a theorem about an operator, first eliminate the operator using its definition, then manipulate, and finally reintroduce the operator (if necessary).
  
  
• Heuristic. To prove P == Q, transform the side with the most structure (either P or Q) into the other.
  
  
• Principle. Structure proofs to minimize the number of rabbits pulled out of a hat --make each step seem obvious, based on the structure of the expression and the goal of manipulation.
  
  
• Principle. Lemmas can provide structure, bring to light interesting facts, and ultimately shorten a proof.
  
  
• Heuristic. Exploit the ability to parse theorems like Golden rule, p & q == p == q == p | q, in many different ways (using associativity and symmetry transparently).