@misc(allaisgit,
 author       = {G. Allais},
 year         = {2018},
 title        = {Deciding Presburger arithmetic in agda},
 url          = {https://github.com/gallais/agda-presburger},
)
@article(mahboubircf,
 author       = {C. Cohen and A. Mahboubi},
 year         = {2012},
 title        = {Formal Prrofs in Real Algebraic Geometry: from Ordered Fields to Quantifier Elimination},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 pages        = {1--40},
 doi          = {10.2168/LMCS-8(1:2)2012},
)
@misc(omega,
 author       = {P. Cr\'{e}gut},
 title        = {Omega: a solver of quantifier-free problems in Presburger Arithmetic},
 url          = {https://coq.inria.fr/refman/omega.html},
)
@article(atdt,
 author       = {J. Doner and W. Hodges},
 year         = {1988},
 title        = {Alfred Tarski and Decidable Theories},
 journal      = {The Journal of Symbolic Logic},
 volume       = {53},
 number       = {1},
 pages        = {20--35},
 doi          = {10.1017/S0022481200028905},
)
@article(ginc,
 author       = {K. G\"{o}del},
 year         = {1931},
 title        = {\"{U}ber formal unentscheidbare S\"{a}tze der Principia Mathematica und verwandter Systeme, I},
 journal      = {Monatshefte f\"{u}r Mathematik und Physik},
 volume       = {38},
 pages        = {173--198},
 doi          = {10.1007/BF01700692},
)
@book(herbrand,
 author       = {J. Herbrand},
 year         = {1971},
 title        = {Logical Writings},
 publisher    = {D. Reidel Publishing Company},
 address      = {Dordrecht, Netherlands},
 doi          = {10.1007/978-94-010-3072-4},
)
@inproceedings(mahboubiacf,
 author       = {A. Mahboubi and C. Cohen},
 year         = {2010},
 title        = {A Formal Quantifier Elimination for Algebraically Closed Fields},
 booktitle    = {Intelligent Computer Mathematics},
 publisher    = {Calculemus 2010},
 address      = {Paris, France},
 pages        = {189--203},
 doi          = {10.1007/978-3-642-14128-7\_17},
)
@article(nipkowjar,
 author       = {T. Nipkow},
 year         = {2010},
 title        = {Linear Quantifier Elimination},
 journal      = {Journal of Automated Reasoning},
 volume       = {45},
 pages        = {189--212},
 doi          = {10.1007/s10817-010-9183-0},
)
@inproceedings(robinson,
 author       = {R. M. Robinson},
 year         = {1950},
 title        = {An Essentially Undecidable Axiom System},
 booktitle    = {Proceedings of the International Congress of Mathematics},
 volume       = {1},
 pages        = {729--730},
)
@techreport(presbryan,
 author       = {R. Stansifer},
 year         = {1984},
 title        = {Presburger's Article on Integer Arithmetic: Remarks and Translation},
 type         = {Technical Report},
 number       = {TR84-639},
 institution  = {Cornell University, Computer Science Department},
 url          = {https://cs.fit.edu/~ryan/papers/presburger.pdf},
)
@article(tarski44,
 author       = {A. Tarski},
 year         = {1944},
 title        = {The semantic conception of truth},
 journal      = {Philosophy and Phenomenological Research},
 volume       = {4},
 pages        = {341--376},
 doi          = {10.2307/2102968},
)
@inproceedings(vanderwalt2,
 author       = {P. van der Walt and W. Swierstra},
 year         = {2012},
 title        = {Engineering Proof by Reflection in Agda},
 editor       = {Ralf Hinze},
 booktitle    = {IFL - 24th International Symposium on Implementation and Application of Functional Languages},
 series       = {Lecture Notes in Computer Science},
 volume       = {8241},
 publisher    = {Springer},
 address      = {Oxford, United Kingdom},
 pages        = {157--173},
 doi          = {10.1007/978-3-642-41582-1\_10},
)
@misc(agda,
 author       = {The Agda Wiki},
 year         = {2017},
 title        = {The Agda Wiki},
 url          = {http://wiki.portal.chalmers.se/agda/pmwiki.php},
)
@misc(agdatut,
 author       = {The Agda Wiki},
 year         = {2017},
 title        = {The Agda Wiki - Tutorials},
 url          = {http://wiki.portal.chalmers.se/agda/pmwiki.php},
)