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

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?

• @GuyCoder why not automatic-theorem-proving?
– Couchy
Feb 11, 2022 at 22:11
• How is disjunction elimination not constructively valid? Coq accepts it without any axioms:Theorem disj_elim (A B : Prop) (hAorB : A \/ B) (hNotA : ~A): B. Proof. destruct hAorB as [hA | hB]. - contradiction (hNotA hA). - exact hB. Qed.
– Maya
Feb 13, 2022 at 13:34
• @NieDzejkob, You're totally right. This inference is valid in IPC. Fixed. Feb 13, 2022 at 14:10

## 1 Answer

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.