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 
be found.

Roger Jones
Proofpower mailing list

Reply via email to