Formalizing Constructive Quantifier Elimination in Agda

Jeremy Pope
(University of Gothenburg)

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.

In Robert Atkey and Sam Lindley: Proceedings of the 7th Workshop on Mathematically Structured Functional Programming (MSFP 2018), Oxford, UK, 8th July 2018, Electronic Proceedings in Theoretical Computer Science 275, pp. 2–17.
Published: 10th July 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: