The proof assistant and the model finder

Are they the dual relation?

The proof assistant is the top down.
The model finder is the bottom up.

I think it is interesting that we iteratively use them.