Sciweavers

Share
CORR
2006
Springer

Combining decision procedures for the reals

9 years 9 months ago
Combining decision procedures for the reals
Abstract. We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which "local" decision or heuristic procedures for fragments of the theory of the reals can be amalgamated into global ones. Let Tadd [Q] be the first-order theory of the real numbers in the language with symbols 0, 1, +, -, <, . . . , fa, . . . where for each a Q, fa denotes the function fa(x) = ax. Let Tmult [Q] be the analogous theory for the language with symbols 0, 1,
Jeremy Avigad, Harvey Friedman
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CORR
Authors Jeremy Avigad, Harvey Friedman
Comments (0)
books