Software for Quantifier Elimination in Propositional Logic

摘要

We consider the following problem of Quantifier Elimination (QE). Given a Boolean CNF formula F where some variables are existen-tially quantified, find a logically equivalent CNF formula that is free of quantifiers. Solving this problem comes down to finding a set of clauses depending only on free variables that has the following property: adding the clauses of this set to F makes all the clauses of F with quantified variables redundant. To solve the QE problem we developed a tool meant for handling a more general problem called partial QE. This tool builds a set of clauses adding which to F renders 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.