素朴な方法
前回のような超越関数を含む論理式を QE する方法として，すぐ思いつくのは近似です．
ここで言う近似とは，一般に述語論理の論理式は自由変数についての条件ですから，それを満たす点の集合をその部分集合（サブセット）と拡大集合（スーパーセット）で評価することです．
論理式は，集合 X(⊆R^n)，X×A(⊆R^n×R^m) で定義された実数値連続関数 p，q を用いて
∀x ( x∈X → p(x)≧q(x，a) )
と表せるものを考えます（＞の場合も同様ですので，これが処理できれば，移項や連言，否定により
∀x ( x∈X → p(x)≦q(x，a) )
∀x ( x∈X → p(x)＝q(x，a) )
∃x ( x∈X → p(x)≧q(x，a) )
∃x ( x∈X → p(x)≦q(x，a) )
∃x ( x∈X → p(x)＝q(x，a) ) （中間値定理による）
も扱えます）．
ポイントは，X，A，q を固定して，この式を満たす点 a の集合（解集合）を S(p) で表すとき
∀x ( x∈X → f(x)≦g(x) )
ならば
S(f)⊆S(g)
が成り立つという性質で，例えば
∀x ( 0≦x≦1 → exp(x)≧ax+b )
の解集合を内外から評価するには，exp 自体を適当な関数で上下から評価すればよいわけです．なお，関数側の誤差の sup ノルムがそのまま集合の境界を表す b ＝ の形の関数の誤差の sup ノルムになります．
評価に用いる関数はもちろん QE できるものでないと困りますから，上の例なら，ひとまず
∀x ( 0≦x≦1 → 1+x+(1/2)x^2≦exp(x)≦1+x+(exp(1)/2)(x^2) )
のように x=1 を中心に評価すると
In[1]:= Reduce[
ForAll[x, 0 <= x <= 1, 1 + x + x^2/2 >= a*x + b], Reals]Out[1]= (a <= 1 && b <= 1) || (1 < a <= 2 &&
b <= 1/2 (1 + 2 a - a^2)) || (a > 2 && b <= 1/2 (5 - 2 a))In[2]:= Reduce[
ForAll[x, 0 <= x <= 1, 1 + x + (E/2)*x^2 >= a*x + b], Reals]Out[2]= (a <= 1 && b <= 1) || (1 < a <= 1 + E &&
b <= (-1 + 2 a - a^2 + 2 E)/(2 E)) || (a > 1 + E &&
b <= 1/2 (4 - 2 a + E))
となるので
a <= 1 && b <= 1
は確定です．同様に
∀x ( 0≦x≦1 → exp(1)+exp(1)(x-1)+(exp(1)/2)(x-1)^2≦exp(x)≦exp(1)+exp(1)(x-1)+x^2 )
のように x=1 を中心に評価すると
a > E && b <= -a + E
が判ります．
ただし，主要部分である 1≦a≦exp(1) について，微分法などで得られる解集合を表す
a - a*Log[a] >= b
を得ることは当然出来ません．ちなみに，x=1/2 を中心に評価した
∀x ( 0≦x≦1 → Exp[1/2] + Exp[1/2] (x - 1/2) - 2 (-2 + Exp[1/2]) (x - 1/2)^2<=Exp[x]<=Exp[1/2] + Exp[1/2] (x - 1/2) - 2 (3 Sqrt[E] - 2 E) (x - 1/2)^2 )
から得られる境界の範囲は
(1 <= a < Sqrt[E] && (
8 a + a^2 - 16 Sqrt[E] - 6 a Sqrt[E] + 9 E)/(-16 + 8 Sqrt[E]) <=
b <= (-a^2 + 14 a Sqrt[E] - 25 E - 8 a E +
16 E^(3/2))/(-24 Sqrt[E] + 16 E)) || (Sqrt[E] < a <=
4 - Sqrt[E] && (
8 a + a^2 - 16 Sqrt[E] - 6 a Sqrt[E] + 9 E)/(-16 + 8 Sqrt[E]) <=
b <= (-a^2 + 14 a Sqrt[E] - 25 E - 8 a E +
16 E^(3/2))/(-24 Sqrt[E] + 16 E)) || (4 - Sqrt[E] <=
a <= -5 Sqrt[E] + 4 E &&
1 - a + Sqrt[E] <=
b <= (-a^2 + 14 a Sqrt[E] - 25 E - 8 a E +
16 E^(3/2))/(-24 Sqrt[E] + 16 E)) || (-5 Sqrt[E] + 4 E < a <= E &&
1 - a + Sqrt[E] <= b <= -a + E)
であり，実際の境界 a - a*Log[a] = b と併せて図示すると
のようになります（緑色＝解集合の部分集合，赤色＝解集合の補集合の部分集合，青色＝解集合の境界）．
今回は，関数の評価にテイラーの定理を用いましたが，誤差を小さくするには次数が大きくせねばなりませんので，区間を分割し各区間における上限，下限による評価から得られた条件の連言をとるといった方法も今後試してみたいと思います．
