[FOM] paper on decision procedures for the reals
Jeremy Avigad
avigad at cmu.edu
Wed Feb 1 17:39:54 EST 2006
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
More information about the FOM
mailing list