Local Theories and Efficient Partial Quantifier Elimination

Abstract

Quantifier elimination is used in various automated reasoning tasks, including quantified SMT solving, exists/forall solving, program synthesis, model checking, and constrained Horn clause (CHC) solving. Complete quantifier elimination, however, is computationally intractable for many theories. The recent algorithm QEL shows a promising approach to approximate quantifier elimination, which has resulted in improvements in solver performance. QEL performs partial quantifier elimination with a completeness guarantee that depends on a certain semantic property of the given formula.

In this thesis, we study local theories, focusing on their proof theoretic and semantic characterization. We identify a subclass of local theories in which partial quantifier elimination can be performed efficiently. By considerably generalizing the previous approach, we present T-QEL, a parametrized polynomial time algorithm that is relatively complete for this class of theories. The algorithm utilizes the proof theoretic characterization of the theories, which is based on restricted derivations. Finally, we prove for T-QEL, soundness in general, and relative completeness with respect to the identified class of theories.