Formalizing Constructive Quantifier Elimination in Agda
Abstract
In this thesis a constructive formalization of quantifier elimination is presented,
based on a classical formalization by Tobias Nipkow [16]. The formalization is implemented
and verified in the programming language/proof assistant Agda [1]. 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.
Degree
Student essay
Collections
View/ Open
Date
2018-04-04Author
Pope, Jeremy
Keywords
Agda
decidability
semantics
successor
constructive
Language
eng