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