A Suite of Cool Logic Programs

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 […]