今回は，第一種 Chebyshev 多項式 $T_4(x)=64x^7-112x^5+56x^3-7x$ に関する $\exists a\ \exists b\ \exists c\ \forall x\ (\, -1\le x\le1 \to 64 x^7+a x^5+b x^3+c x\le m\,)\quad \cdots\quad (*)$ が $1\le m $ と等価であるという性質です．まず $\f…

A.W.Strzebonski "Cylindrical Algebraic Decomposition using validated numerics" の 7.2. Randomly generated systems で使用された入力です．元の code では CylindricalDecomposition ですが，変数順序を heuristic に委ねるため，無指定の Reduce で実…

CAD において，変数順序の選定は非常に重要です． 例えば ? projs([x1,x2,x3,x4],[-218 + 955*x1^2*x2*x3 + 520*x2*x3^3 + 1017*x3^4 + 250*x1*x2*x4 - 391*x2^3*x4 - 525*x1*x3*x4^2]); *** using Lazard's method (MPP17). [x4,1] [x3,3] [x2,4] [x1,4] ti…

今回は「 $x^3+y^3=a,\ 1\le x\le y$ を満たす格子点 $(x,\ y)$ の個数が $4$ である」ような $a$ の最小値，および，それに対応する $4$ 個の格子点を求める問題です．処理時間とメモリーとのバランスから，適当な上界を与え，出現をカウントしつつ，$x^3+y…

Quantified Formula: QE(forall a b c d) ((a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0 and -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -…

$\exists a\ \exists b\ \exists c\ \forall x\ \forall y\ [\ \neg[a=0 \land b=0] \land\, [\,ax+by+c=0\ \to\ dx^2+exy+fy^2=1\,]\,]$ C.W.Brown "Simple CAD Construction and its Applications" ? tst12([ex,ex,ex,all,all],[d,e,f,a,b,c,x,y],(f1,f2,f…