wdls

Uses the DLS algorithm to find a witness for a predicate elimination problem of the form ∃X₁ ... ∃Xₙ φ where φ is a first order formula and X₁,...,Xₙ are second-order variables.

If the method succeeds, the return value is a substitution of the variables in the input predicate elimination problem such that applying the substitution to φ gives a first-order formula which is equivalent to ∃X₁ ... ∃Xₙ φ.

A sufficient criterion for the success of the method is φ can be put into the form

(α_1(X) ∧ β_1(X)) ∨ ... ∨ (α_n(X) ∧ β_n(X))

where

• no occurrences of X are inside the scope of a first-order existential quantifier,
• α_i(X) is positive with respect to X and β_i(X) is negative with respect to X and
• for every i either
• α_i(X) does not contain X or
• β_i(X) does not contain X or
• every disjunction in α_i(X) ∧ β_i(X) contains at most one occurrence of X

by

• simplifying φ,
• moving quantifiers as far down as possible to reduce their scope and
• distributing conjunctions over disjunctions in subformulae where positive and negative occurrences of X are not already separated by a conjunction.

The method solves the problem for multiple variables by successive elimination of a single variable starting with Xₙ, then X_{n-1} and so on.

A Failure return value does not mean that the quantifier elimination is impossible. It just means that this algorithm could not find a witness which allows elimination of the second order quantifier.