Once you are past propositional logic the workhorse is rewriting (which uses
equations to transform a theorem or goal), and of course induction is important
when working with inductively definable structures like the natural numbers.
Use the KWIC index in the reference manual to find rules (if you are sticking
with forward proof) including the words "rewrite" or "induction" or look up
these topics in the tutorial notes USR013 where some examples and exercises can
Proofpower mailing list