New approaches to boolean quantifier elimination
Christoph Zengler, Andreas Kübler, Wolfgang Küchlin · ACM communications in computer algebra · 2011
We present four different approaches for existential Boolean quantifier elimination, based on model enumeration, resolution, knowledge compilation with projection, and substitution. We point out possible applications in the area of verification and we present preliminary benchmark results of the different approaches.