正射影で QE - ATPとCASのこと

　前回，前々回のような解集合の図は，束縛・自由変数が合わせて 3 種類以下なら，与えられた論理式から簡単に求められます．
　例えば，自由変数が 2 種類，束縛変数が 1 種類の特称量化論理式

$(1)\;\exists z\,P(x,y,z)$

を満たす点 $(x,y,0)$ とは，その点を通って $xy$ 平面に垂直な直線上に $P(x,y,z)$ を満たす点 $(x,y,z)$ が存在するような点，つまり，その直線と空間図形 $P(x,y,z)$ に共有点が存在するような点のことですから， $(1)$ の解集合は空間図形 $P(x,y,z)$ の $xy$ 平面への正射影です．従って，全称量化論理式

$\forall z\,P(x,y,z)\equiv\neg(\,\exists z\,\neg(P(x,y,z))\,)$

の解集合は空間図形 $\neg(P(x,y,z))$ の $xy$ 平面への正射影の（ $xy$ 平面に対する）補集合です．
　よって，前回の

$\forall x\;(\; -1\le x\le 1\,\to\,a_1 x e^x \,+\,a_2 x^3 \cos \pi x\,+\,\frac{1}{\log\left(x^2+2\right)}\,> 0\;)$

の解集合は，空間図形

$-1\le x\le 1\;$ ∧ $\;a_1 x e^x \,+\,a_2 x^3 \cos \pi x\,+\,\frac{1}{\log\left(x^2+2\right)}\le 0$

の $a_1a_2$ 平面への正射影の補集合なので，その図は

RegionPlot3D[
E^x x a[1] + x^3 a[2] Cos[\[Pi] x] + 1/Log[2 + x^2] <= 0,
{a[1], -1, 5}, {a[2], -2, 12}, {x, -1, 1},
ViewPoint -> {0, 0, +Infinity}, PlotPoints -> 100]

の出力