The KeYmaera tool is a theorem prover to verify hybrid systems, based on the KeY tool. In 2009, I had the pleasure to work with the KeYmaera guys on the decision procedures for real-closed fields (which is more or less the same as the theory of real numbers) that are integrated in KeYmaera. In particular, we investigated the usage of Stengle's Positivstellensatz and the Real Nullstellensatz to decide the universal fragment of the first-order theory of real-closed fields.
The work is described in this paper, a more detailed version of which has appeared as a technical report.