Playing wth Quantifiers

Quantifiers

Quantifiers are fundamental logical operators that express properties over sets of values:

  • Universal Quantifier (∀): expresses that a property holds for all values

  • Existential Quantifier (∃): expresses that a property holds for at least one value

Solving General Quantified Problems

The basic idea of quantifier instantiation is to replace a quantified formula with a finite set of instances that are obtained by substituting concrete terms for the quantified variables.

Instantiation Techniques

  1. E-matching:

  2. Model-based: MBQI (model-based quantifier instantiation)

  3. Enumerative:

Some useful tools: - https://github.com/viperproject/axiom-profiler-2

Solving Exists-Forall Problems

Quantifier Elimination

Quantifier elimination refers to the process of eliminating the quantifiers from a formula by constructing an equivalent quantifier-free formula.

We can apply Skolemization to remove the \(\exists\) quantifiers. After that, it is sufficient to instantiate the \(\forall\) quantifiers for each constant. For example, \(\forall x: T\ A\) becomes \(A[c_1/x] \land A[c_2/x] \land \ldots\). The result is equi-satisfiable and quantifier-free.

It is important to understand the differences between Skolemization and quantifier elimination:

  • First, Skolemization does not preserve the formula’s meaning (it preserves satisfiabilty, but not equivalence)

  • Second, QE replaces a formula with an equivalent but quantifier-free formula

  • Third, QE is only possible for specific theories, and is generally very expensive