2018/07/11 by Jeremy Pope
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.275.2
published as EPTCS 275, 2018, pp. 2-17 · In Proceedings MSFP 2018, arXiv:1807.03732
arxiv created 2018/07/11 · arxiv updated 2018/07/12
In this paper a constructive formalization of quantifier elimination is presented, based on a classical formalization by Tobias Nipkow. The formalization is implemented and verified in the programming language/proof assistant Agda. It is shown that, as in the classical case, the ability to eliminate a single existential quantifier may be generalized to full quantifier elimination and consequently a decision procedure. The latter is shown to have strong properties under a constructive metatheory, such as the generation of witnesses and counterexamples. Finally, this is demonstrated on a minimal theory on the natural numbers.