Please note: This master’s thesis presentation will take place in DC 2310 and online.
Estifanos Getachew, Master’s candidate
David R. Cheriton School of Computer Science
Supervisors: Professors Arie Gurfinkel, Richard Trefler
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.
To attend this master’s thesis presentation in person, please go to DC 2310. You can also attend virtually on Zoom.