# Software for Quantifier Elimination in Propositional Logic

Eugene Goldberg and Panagiotis Manolios.

*ICMS*, 2014

# Abstract

We consider the problem of Quantifier Elimination (QE): given a
Boolean CNF formula F where some variables are existentially
quantified, find a logically equivalent quantifier-free CNF
formula. This problem can be solved by finding a set of clauses
containing only free variables such that adding this set of clauses
to F makes all of the clauses of F containing quantified variables
redundant. To solve the QE problem we developed a tool that handles a
more general problem called partial QE. Our tool generates a set of
clauses that when added to F render a specified subset of clauses with
quantified variables redundant. In particular, if the specified
subset contains all the clauses with quantified variables, our tool
performs QE.

PDF