Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentationrealsrldpep

rldpep – deciding polynomial exponential problems

Calling Sequence

rldpep \((\,\varphi\,)\)
rldpep \((\,\varphi\,,\ n\,)\)

Arguments

\(\varphi\) polynomial exponential sentence
\(n\) positive integer

Returns

\(\varphi′\) one of the truth values true, false

Description

The notion of polynomial exponential problems refers to an extension of the theory of real closed fields. Polynomial exponential sentences are constructed as follows: In the theory of real closed fields, consider a formula \(\psi\) with exactly one free variable \(y\), and assume that the variable \(x\) does not occur in \(\psi\). Then polynomial exponential sentences \(\varphi\) are obtained from \(\psi\) by substituting \(e^x\) for \(y\) and introducing an outmost existential or universal quantifier for \(x\). Formally: \[ \varphi = \exists x \psi[y \gets e^x] \quad \text{or} \quad \varphi = \forall x \psi[y \gets e^x]. \]

Technically, the exponential function is accepted in the input in the form e^x for one variable x. More generally, as \(e^{kx}=(e^x)^k\), the input may contain e^(\(k\)*x) for \(k=1,2,\dots\)

It is noteworthy that one polynomial exponent can be logically encoded by the introduction of a helper variable. For instance, for equating a Gaussian function to a polynomial \(p(x)\) one could go \(\exists z \exists x(z=-x^2 \land e^z=p(x)).\)   In the same way, \(e^{-x}\) can be encoded but then not be combined with, say, \(e^x\). Nevertheless, the concept of polynomial exponential problems is strong enough to encode nontrivial occurrences of \(\cosh(x)=(e^x+e^{-x})/2.\)   For instance, for some polynomial \(p(x)\) \[ \forall x(x>7 \longrightarrow \cosh(x)>p(x)) \] can be equivalently rewritten as \(\forall x(x>7 \longrightarrow e^{2x}+1 > 2p(x)e^x).\)

During the decision procedure, lower and upper bounds for the exponential series are computed using truncated Taylor series expansions of the exponential function. The optional parameter \(n\) specifies the number of summands of the Taylor series computed for that purpose. The default is \(n=20.\)   When the chosen accuracy is not sufficient, this is recognized by the procedure, and a corresponding error message is thrown. The computation can then be repeated with a larger choice for \(n\). Note, however, that increasing the accuracy considerably slows down the computation.

Before the actual decision of the outermost quantifier, whose variable occurs within the scope of the exponential function, all inner quantifiers are eliminated using rlcad.

Examples

rldpep ex({x, y, z}, (x-1)*(x-2)=0 and 2*x+y-z=0 and e^(2*x)*y-x*z=0);
rldpep ex({z, x}, 10*e^z=-8*x^2+10 and x <> 0 and z+x^2=0);
rldpep all(x, x>7 impl e^(2x)+1>2*e^x*x^3-8*x*e^x);
rldpep(all(x, x>7 impl e^(2x)+1>2*e^x*x^3-8*x*e^x), 50);

Switches

⊕ = on by default, ⊖ = off by default

See Also

References

  1. M. Achatz. Deciding polynomial-exponential problems. Diploma Thesis. Universit├Ąt Passau, 2006.
  2. M. Achatz, S. McCallum, and V. Weispfenning. Deciding polynomial-exponential problems. Proc. ISSAC 2008, ACM Press, 2008.