[FOM] paper on decision procedures for the reals

[Jeremy Avigad]

I have posted a preliminary version of a paper I have written with 
Harvey Friedman, "Combining decision procedures for the reals," on my 
home page,

   http://www.andrew.cmu.edu/~avigad

under "Research".

The paper considers, roughly, the union of the additive and 
multiplicative fragments of the theory of the real numbers as an ordered 
field. This can, alternatively, be viewed as the theory of real closed 
fields minus distributivity.

There are two reasons for considering such theories. The first is that 
they seem to capture many of the straightforward inferences that come up 
in verifying ordinary mathematical texts. The second is that they 
provide a good example of what can happen when one tries to "amalgamate" 
simple decision procedures in theories with nontrivial overlap, a task 
that is generally important to automated reasoning.

We have a number of interesting results. In particular, the full union 
of the additive and multiplicative theories described above is 
undecidable, but the universal fragment is decidable. Our decision 
procedures are not practical, but we provide concrete suggestions 
towards developing heuristic procedures that, we expect, will work well 
in practice.

Jeremy