@inproceedings{10.1007/978-3-642-57201-2_32,
    Abstract = {We present a decision procedure for linear-transcendental problems formalized in a suitable first-order language. The problems are formalized by formulas with arbitrary quantified linear variables and a block of quantifiers 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. Potential applications include reachability problems for linear differential systems.},
    Address = {Berlin, Heidelberg},
    Author = {Weispfenning, Volker},
    BookTitle = {Computer Algebra in Scientific Computing},
    Editor = {Ganzha, Victor G. and Mayr, Ernst W. and Vorozhtsov, Evgenii V.},
    ISBN = {978-3-642-57201-2},
    Pages = {423--437},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Deciding Linear-Transcendental Problems},
    Year = {2000},
    date-added = {2018-09-03 14:51:00 +0000},
    date-modified = {2018-09-03 14:51:00 +0000},
    doi = {10.1007/978-3-642-57201-2_32}
}

@inproceedings{10.1007/978-3-642-57201-2_32, Abstract = {We present a decision procedure for linear-transcendental problems formalized in a suitable first-order language. The problems are formalized by formulas with arbitrary quantified linear variables and a block of quantifiers 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. Potential applications include reachability problems for linear differential systems.}, Address = {Berlin, Heidelberg}, Author = {Weispfenning, Volker}, BookTitle = {Computer Algebra in Scientific Computing}, Editor = {Ganzha, Victor G. and Mayr, Ernst W. and Vorozhtsov, Evgenii V.}, ISBN = {978-3-642-57201-2}, Pages = {423--437}, Publisher = {Springer Berlin Heidelberg}, Title = {Deciding Linear-Transcendental Problems}, Year = {2000}, date-added = {2018-09-03 14:51:00 +0000}, date-modified = {2018-09-03 14:51:00 +0000}, doi = {10.1007/978-3-642-57201-2_32} }