You may have heard about the Tarski-Seidenberg theorem, which says that the first-order theory of the reals is decidable, that the first-order theory of the complex numbers is similarly decidable, or that the first order theory of the integers without multiplication is decidable.

In the course of John Harrison‘s logic textbook Handbook of Practical Logic and Automated Reasoning, all three of these algorithms (and many more) are implemented. Furthermore, you can download and play with them for free. (However, I still recommend checking out the book: especially if you are looking for a good textbook for a course on logic with a concrete, computational bent.)

Below, I’ll describe how to install the programs and try them out. There are many more interesting functions in this suite that I haven’t described.