I know of a handful of automated theorem provers for classical first-order logic such as Vampire (source code).
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?
Theorem disj_elim (A B : Prop) (hAorB : A \/ B) (hNotA : ~A): B. Proof. destruct hAorB as [hA | hB]. - contradiction (hNotA hA). - exact hB. Qed.$\endgroup$