...somehow my last post got garbled...maybe because of the html link?
So instead, here is link to just the Equational Logic "rules of inference"
And a sample of the proof I would like to encode in ProofPower:
I have been studying the idea of "equational logic" as described in this
> link by Gries and wonder if anyone has used ProofPower in this way. If so,
> I would love to see a sample.
> One reason for my interest in this approach is because it seems more in
> line with proof by induction (which is a major topic of Discrete Math).
> For example, to prove that 2^n > n^2 for n >= 4 using induction seems like
> it would be clearest using equational logic.
Proofpower mailing list