
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).
