1 2 3 x

Inductive Properties of Lists, Part 1
Final Remarks

 This proofweb is a good demonstration of the way that failed proof attempts can suggest what to do next in a term reduction based approach to theorem proving. We started (see the proof homepage) trying to prove a result which looked simple, but which in fact required two lemmas. With a little analysis, we were able to formulate a lemma which we hoped would complete the proof, and our attempt to prove it then led to the discovery of the second lemma. Of course, these remarks can only be validated by showing that trying to prove these three results in the reverse order of that in which they were discovered does in fact prove the original goal; this is done in our second proofweb for this goal. On the other hand, it should not be expected that things will always be so easy; for example, if our initial goal were to prove Fermat's Last Theorem, then a proof attempt by induction on the exponent (or any other variable) would not yield a useful lemma.

This page was generated by Kumo on Mon Nov 20 10:18:44 PST 2000.