C. Cohen & A. Mahboubi (2012):
Formal Prrofs in Real Algebraic Geometry: from Ordered Fields to Quantifier Elimination.
Logical Methods in Computer Science 8,
pp. 1–40,
doi:10.2168/LMCS-8(1:2)2012.
J. Doner & W. Hodges (1988):
Alfred Tarski and Decidable Theories.
The Journal of Symbolic Logic 53(1),
pp. 20–35,
doi:10.1017/S0022481200028905.
K. Gödel (1931):
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.
Monatshefte für Mathematik und Physik 38,
pp. 173–198,
doi:10.1007/BF01700692.
J. Herbrand (1971):
Logical Writings.
D. Reidel Publishing Company,
Dordrecht, Netherlands,
doi:10.1007/978-94-010-3072-4.
A. Mahboubi & C. Cohen (2010):
A Formal Quantifier Elimination for Algebraically Closed Fields.
In: Intelligent Computer Mathematics.
Calculemus 2010,
Paris, France,
pp. 189–203,
doi:10.1007/978-3-642-14128-7_17.
T. Nipkow (2010):
Linear Quantifier Elimination.
Journal of Automated Reasoning 45,
pp. 189–212,
doi:10.1007/s10817-010-9183-0.
R. M. Robinson (1950):
An Essentially Undecidable Axiom System.
In: Proceedings of the International Congress of Mathematics 1,
pp. 729–730.
R. Stansifer (1984):
Presburger's Article on Integer Arithmetic: Remarks and Translation.
Technical Report TR84-639.
Cornell University, Computer Science Department.
Available at https://cs.fit.edu/~ryan/papers/presburger.pdf.
A. Tarski (1944):
The semantic conception of truth.
Philosophy and Phenomenological Research 4,
pp. 341–376,
doi:10.2307/2102968.
P. van der Walt & W. Swierstra (2012):
Engineering Proof by Reflection in Agda.
In: Ralf Hinze: IFL - 24th International Symposium on Implementation and Application of Functional Languages,
Lecture Notes in Computer Science 8241.
Springer,
Oxford, United Kingdom,
pp. 157–173,
doi:10.1007/978-3-642-41582-1_10.
eptcs@eptcs.org