> > It would be nice if everyone could master these > > "abstractions" and the basic methods of proof, but > few > > are motivated to do so. I hope my little video and > my > > software will help a bit in this regard. > > I'm not sure why students at large would be > interested in formal predicate calculus based proofs,
Alas, they probably wouldn't be.
> but for the smaller populations that are, it seems a > shame to not include the fundamental fact that once a > formal system is adopted, the very act of generating > proofs can be automated
The verification of formal proofs, by definition, can be automated. The GENERATION of formal proofs in predicate calculus and mathematics in general has only been partially automated, however. Proof writing is still very much a creative exercise of the highest order.