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
(Warning: I've never actually done much of this before so some details might be wrong.)