First order logic is undecidable, so SAT solving does not really help. That said, techniques exist for bounded model checking of first order formulas. This means that only a fixed number of objects can be considered when trying to determine whether the formula is true or false. Clearly, this is not complete, but if a counter-example is found, then it truly is a counter-example.
The tool Alloy is one tool that allows models to be described in first-order logic (though the surface syntax is based on relationally described models) and uses bounded model checking to find solutions. A SAT solver is used under the hood. One alloy extension allows models with a temporal character, though technically it does not support temporal logic.
If you wish to explore further, for example, to verify program correctness, then you can look at program verification tools. These are generally based on Hoare logic (for reasoning about pre- and post-conditions), possibly extended with Separation logic (for reasoning about heaps). These logics are generally undecidable, so a certain amount of interaction between the human and the verification tool is required.
Some example tools are: