using [[simp_trace]] let's you see what simplification rules were used and using [[unify_trace_failure]] let's you see what unification issues were encountered. I wonder if resolution proofs can be equally traced. This would make Isabelle proofs effectively surveyable.
I don't think one can trace auto, blast,... step by step or get proof scripts from them. (this mailing list thread should be interesting for you). What you can do is get a list of the used facts, for more details see davidgs answer in this thread.