Are there automated theorem provers for constructive logics? What strategy do they use?

Question

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?

Answer 1

The firstorder tactic in Coq is an "experimental extension of tauto to first-order reasoning." The tauto tactic "implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92]". Perhaps one of the Coq developers can speak to the theory behind firstorder.

These tactics do not rely on classical axioms, and do generate proof terms.