|
Abstract : |
We present a decision procedure for linear-transcendental problems formalized in a suitable rst-order language. The problems are formalized by formulas with arbitrary quantied linear variables and a block of quantiers with respect to mixed linear-transcendental variables. Variables may range both over the reals and over the integers. The transcendental functions admitted are characterized axiomatically; they include the exponential function applied to a polynomial, hyperbolic functions and their inverses, and the arcustangent. The decision procedure is explicit and implementable; it is based on mixed real-integer linear elimination, the symbolic test point method, elementary analysis, and Lindemann's theorem. As a byproduct we obtain sample solutions for existential formulas and a qualitative description of the connected components of the satisfaction set wrt. a mixed linear-transcendental variable., |
