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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
