Internally, I think most of these provers work by translating premises and the negated goal into disjunctions of literals and then applying resolution. This also requires Skolemization as a preprocessing step, which removes existential quantifiers in the prenex of a wff and adds new function symbols to the language. Here's a link to the the Skolemization implementation in Vampire.
This technique will not work in a constructive setting. Negating the goal, converting to negative normal form and then prenex normal form is not constructively valid.
What automated theorem provers for intuitionistic first-order logic are there (whether they're capable of emitting proof terms or not)? If there are any, broadly speaking, what strategy do they use?