Quantifier Elimination and Provers Integration
Silvio Ghilardi · Electronic Notes in Theoretical Computer Science · 2003
We exploit quantifier elimination in the global design of combined decision and semi-decision procedures for theories over non-disjoint signatures, thus providing in particular extensions of Nelson-Oppen results.