1 paper
Jeremy Pope
In this paper a constructive formalization of quantifier elimination is presented, based on a classical formalization by Tobias Nipkow. The formalization is implemented and verifie…