A very long time ago I taught an elementary course that covered what was called natural deduction<https://docs.google.com/viewer?url=http%3A%2F%2Fwww.danielclemente.com%2Flogica%2Fdn.en.pdf>. 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.
*-- Russ Abbott* *_____________________________________________* * Professor, Computer Science* * California State University, Los Angeles* * Google voice: 747-*999-5105; CS Dept.: 323-343-6690 Google+: *http://GPlus.to/RussAbbott <http://GPlus.to/RussAbbott>,* * http://tinyurl.com/RussAbbott <http://tinyurl.com/RussAbbott>, or * * http://google.com/+RussAbbottCa <http://google.com/+RussAbbottCa> * * vita: *sites.google.com/site/russabbott/ *CS Wiki* <http://cs.calstatela.edu/wiki/> and the courses I teach * A draft of "Abstractions and Implementations <http://philpapers.org/rec/ABBAAI>" * * How the Fed can fix the economy (**2 pages)**: ssrn.com/abstract=1977688 <http://ssrn.com/abstract=1977688>* *_____________________________________________* On Tue, Dec 17, 2013 at 8:20 PM, Owen Densmore <[email protected]> wrote: > Lovely tweet! > > > <https://twitter.com/i/redirect?url=https%3A%2F%2Ftwitter.com%2FCompSciFact%2Fstatus%2F412987113257570305&sig=2f5397789e4fe174bc127f7f0a3963cefa9553d2&uid=15752750&iid=735ea3c7a31f412bb787bdac118d8509&nid=151+1262&t=1> > Computer > Science > <https://twitter.com/i/redirect?url=https%3A%2F%2Ftwitter.com%2FCompSciFact%2Fstatus%2F412987113257570305&sig=2f5397789e4fe174bc127f7f0a3963cefa9553d2&uid=15752750&iid=735ea3c7a31f412bb787bdac118d8509&nid=151+1264&t=1> > @CompSciFact<https://twitter.com/i/redirect?url=https%3A%2F%2Ftwitter.com%2FCompSciFact%2Fstatus%2F412987113257570305&sig=2f5397789e4fe174bc127f7f0a3963cefa9553d2&uid=15752750&iid=735ea3c7a31f412bb787bdac118d8509&nid=151+1264&t=1> > > > A proof is an algorithm for moving from one proposition to another. > 04:46 PM - 17 Dec > 13<https://twitter.com/CompSciFact/status/412987113257570305> > > > > > > > > > > > > ============================================================ > 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 >
============================================================ 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
