Quantifier Instantiation

Quantifier instantiation:

  • given a conjunct $\forall x.F(x)$ and a term $t$ occurring in other conjuncts, generate $F(t)$ and continue
  • in general this is incomplete
  • it cannot be complete because quantified combination of linear arithmetic with uninterpreted functions symbols is highly undecidable

Triggers: instantiate e.g. $\forall x. P(x) \rightarrow Q(x)$ only if you find $P(t)$

Traditionally resolution-based provers have more sophisticated quantifier handling (but have no decision procedures). This is changing and both approaches integrate techniques from others.

Some approaches combine DPLL(T) solvers and resolution-based solvers

  • SPASS+T by Virgile Prevosto and Uwe Waldmann