1
$\begingroup$

Does quantifier elimination (QE) preserve equi-satisfiability or equivalence?

I always thought it preserves equi-satisfiability (and not equivalence) but in the book [Bradley, Manna], they say both Cooper's method (for Presburger arithmetic) and Ferrante-Rackoff (for rational arithmetic), which are QE methods, preserve equivalence.

So, does QE always preserve equivalence? Are there QE methods that preserve equi-satisfiability and others that preserve equivalence? In such case, any example of both types?

Reference

[Bradley, Manna] The Calculus of Computation, https://community.wvu.edu/~krsubramani/courses/backupcourses/dm2Spr2013/coursetext/CalcofComp.pdf

$\endgroup$

0

You must log in to answer this question.