Refiners are used to develop Proofs top-down, but of course they can be used after-the-fact to validate a whole Inference Step by computing what the premises should be according to refinement, then comparing the actual premises to the expected ones.
Many refiners are Tactic based provers.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html