QE で代入

　今回は QE の立場から「代入」を考えます．

　よく知られた CAS（計算機代数システム）には代入のコマンドが実装されており，例えば，y=x^3+x^2 の x に 2 を代入した式を得るには，Reduce では

sub( x=1 , y=x^3+x^2 );

Mathematica では

ReplaceAll[ y==x^3+x^2 , x -> 1 ]

または

y==x^3+x^2 /. x -> 2

Maple では

subs( x=1 , y=x^3+x^2 ) ;

maxima では

ratsubst( 1, x, y=x^3+x^2 );

とすればよく，何れも y=2 （ Mathematica では y==2 ）と出力されます．

　この y=2 は「 x^3+x^2 の x に 1 を代入したものが y である」という y についての条件ですから，論理式では

∃x [ x=1 ∧ y=x^3+x^2 ]

RedLog では

ex ( x , x=1 and y=x^3+x^2 );

と表せ，これを

rlqe ex ( x , x=1 and y=x^3+x^2 );

のように QE すれば y=2 が得られます．この方法によれば，例えば，x^5+x-1=0 の唯一の実数解を代入するのも

rlqepcad ex ( x , x^5+x-1=0 and y=x^3+x^2 );

のように容易です．

（結果が簡単になる理由は，方程式の左辺を因数分解すれば判ります）

　代入する値が連立方程式の解である場合，解を伏せたまま実行できる QE は特に効果的で，次回はその実例を挙げたいと思います．