QE で解く
今回は「問題を解く」とはどういうことなのかを QE の立場から見てみます．
xy 平面上の楕円 x^2+3y^2=4 と直線 x+3y=k が異なる 2 点 A，B で交わるとき，3 角形 ABC の面積を S とおく．ただし，C(1，1) とする．
このとき，S を k を用いて表し，S が最大となる k の値，および，そのときの S の値を求めよ．
普通に「解く」なら，楕円と直線の式を連立して A，B の座標を求め，C の座標と合わせて面積の公式（？）に代入，得られた式が定める k の関数の極値を微分法などを用いて求める，といった流れとなり，標準的な CAS なら，それを実行することはさして困難ではないでしょう．しかし，それでは人間が行う作業を CAS にやらせているだけで，何の面白みもありません．
我々が理解すべきことは
問題で与えられた定義を論理式で表し，それを QE したものが「答え」である
という事実であり
という認識を持って以下のように処理すれば，我々は「解法」から解放されます．
すなわち，S が 3 角形 ABC の面積になるための条件は，楕円と直線の式をみたす実数の対が丁度 2 個存在して，それらを (a,b),(c,d) とおくと S=|(a-1)(d-1)-(b-1)(c-1)|/2 が成り立つことなので
Reduce[
Exists[
{a, b, c, d},
a^2 + 3 b^2 == 4 && a + 3 b == k &&
c^2 + 3 d^2 == 4 && c + 3 d == k && a != c &&
S == Abs[(a - 1) (d - 1) - (b - 1) (c - 1)]/2
],
Reals
]
のように Mathematica で QE すると
-4 < k < 4 && S == Sqrt[(-(k - 4)^3)*(k + 4)]/(4*Sqrt[3])
と出力され，これを k の関数 S を定義する論理式と見て，値域の定義に従い
Reduce[ Exists[k,%] , Reals ]
のように QE すれば
0 < S <= 3
と出力されます．この結果のみを得たいなら，最初から
Reduce[
Exists[
{a, b, c, d, k},
a^2 + 3 b^2 == 4 && a + 3 b == k &&
c^2 + 3 d^2 == 4 && c + 3 d == k && a != c &&
S == Abs[(a - 1) (d - 1) - (b - 1) (c - 1)]/2
],
Reals
]
とすればよく，RedLog でも
rlslfq rlqe
ex({a,b,c,d,k},
and(a^2+3*b^2=4,a+3*b=k,
c^2+3*d^2=4,c+3*d=k,a<>c,
4*s^2=( (a-1)*(d-1)-(b-1)*(c-1) )^2,s>=0
)
);
とすれば
4924There were 4925 QEPCADB calls!
s - 3 <= 0 and s > 0
と出力されます．
