15
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ @GuyCoder why not automatic-theorem-proving? $\endgroup$
    – Couchy
    Feb 11, 2022 at 22:11
  • 1
    $\begingroup$ 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. $\endgroup$
    – Maya
    Feb 13, 2022 at 13:34
  • $\begingroup$ @NieDzejkob, You're totally right. This inference is valid in IPC. Fixed. $\endgroup$ Feb 13, 2022 at 14:10

1 Answer 1

10
$\begingroup$

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.

$\endgroup$
1

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.