計算の例（３）

「線形変換(p,q)|->(p+aq,p+q)による円板p^2+q^2<=1の像に(x,y)が属する」という式の入力と出力です．RedLog

rlgsn(rlqe( ex({p,q},x=p+a*q and y=p+q and p^2+q^2<=1) ))

QEPCAD B

(a,x,y,p,q) 3 (E p)(E q)[x=p+a q /\ y=p+q /\ p^2+q^2<=1].

Mathematica

FullSimplify[Reduce[Exists[{p,q},x==p+a*q && y==p+q && p^2+q^2<=1],{x,y},Reals]]

この例は簡単すぎて？Mathematicaの陽関数表示が裏目に出ており，RedLog，QEPCAD BのTarski formulaのままが見易いです．RedLogではa<>1でないつまりa=1という条件を用いて最初の式をx-y=0まで整理して欲しいところです．QEPCAD Bは例によって考え過ぎでRedLogが僅か数秒で答えたのに対して…．一方，我等がRisa/Asir（ Risa/Asir - Wikipedia ）は

qe(ex(p,ex(q,x@==p-a*q @&& y@==p+q @&& p^2+q^2@<=1)));
( (y^2-2 @<= 0) @&& (2*x^2+(2*a-2)*y*x+(a^2+1)*y^2-a^2-2*a-1 @== 0) @&& ((2*a+2)*x+(a^2-1)*y @<= 0) ) @||
( (y^2-2 @<= 0) @&& (2*x^2+(2*a-2)*y*x+(a^2+1)*y^2-a^2-2*a-1 @== 0) @&& ((2*a+2)*x+(a^2-1)*y @>= 0) ) @||
( (a+1 @!= 0) @&& (2*x^2+(2*a-2)*y*x+(a^2+1)*y^2-a^2-2*a-1 @<= 0) )

と健闘しています．