A very long time ago I taught an elementary course that covered what was called
natural deduction. It had rules for transforming expressions into other expressions using so-called introduction and elimination rules that allowed you to introduce or eliminate operations such as and, or, etc. and quantifiers. At the time it struck me that a proof in that system was indeed an algorithm for transforming one expression or set of expressions into another. The link above is the sort of thing we did.
============================================================
FRIAM Applied Complexity Group listserv
Meets Fridays 9a-11:30 at cafe at St. John's College
to unsubscribe
http://redfish.com/mailman/listinfo/friam_redfish.com