4 ms·
A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to
by chess93 8y ago
A computer just does symbolic manipulation according to a list of rules (axioms) and the human/programmer specifies which sequence of symbolic manipulations to apply and then the computer simply states whether or not the specified manipulations transform the theorem in to the truth symbol.
http://us.metamath.org/mpegif/mmcomplex.html http://us.metamath.org/mpegif/mmcomplex.html
(Warning: I've never actually done much of this before so some details might be wrong.)
- dwheeler 8y agoI have done some, thanks for pointing to that page! Here's a prettier version for most people (the "mpegif" version uses GIFs for math symbols, which works everywhere but doesn't look at nice): http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html