Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Software for Quantifier Elimination in Propositional Logic

Eugene Goldberg and Panagiotis Manolios.
ICMS, 2014


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.