このブログの第一話？RedLogの巻は如何だったでしょうか？ インストールから基本的な使い方，主要な関数やスイッチ，その他，一通りのことは書いたつもりです．RedLogは，高い拡張性と多彩な関数，オプションスイッチを持ちながら，非常に軽快で使い易いパッ…

これまで述べた以外に，ユーザーが関数を書く際に便利な道具も用意されており，例えば f:=ex(b,all({x,y},x^2+a*x*y+y^2=1 impl x^2+y^2 に含まれる自由変数と束縛変数，原始論理式，項のリスト，および，fの構造は rlvarl(f); {{a},{b,x,y}} rlatl(f); {a*x…

原始論理式（論理記号を含まない論理式）は基本的には多項式についての方程式と不等式であり，これはQEの処理原理から来る制約です．ただし，実際のCASでは幾つかの拡張が見られ，RedLogの場合，デフォルトでは x>a/b; *****(greaterp x (quotient a b)) inv…

ことがあります．例えば，x^2+y^2=1を満たす任意の実数x，yがax^2+cxy+by^2=1を満たす条件 all({x,y},x^2+y^2=1 impl a*x^2+c*x*y+b*y^2=1) をrlqeでQEして，rlgsnで簡約すると即座に a - 1 > 0 and b - 1 = 0 and c = 0 or a - 1 = 0 and b - 1 = 0 and c =…

には互いに他を補う部分があります．例えば x=a+b+c，y=ab+bc+ca，z=abc，a^3+b^3+c^3=1 を満たす実数a，b，cが存在する条件をRedLogに rlqe(ex({a,b,c},and(x=a+b+c,y=a*b+b*c+c*a,z=a*b*c,a^3+b^3+c^3=1))); と尋ねると，１０秒足らずで 5*x**6 - 24*x**4*…

「xを0に近づけたときのsin(x)/xの極限値がyである」という式の入力と出力です．RedLog rlqe(rlcnf(rlpnf( all(p,p>0 impl ex(q,q>0 and all({x,s,c},(0<x<q and 0<s<x and 0<c*x<s and c^2+s^2=1) impl (y-p)*x<s<(y+p)*x))) ))); 8*y**2 + 8*y + 1 > 0 and 8*y**2 - 8*y + 1 > 0 and 8*y**2 - 8*y - 1 0 and 2*y**2 - 3 そして rlqe(ex(y,8*y**2 + 8*y +</x<q>…

「線形変換(p,q)|->(p+aq,p+q)による円板p^2+q^2 rlgsn(rlqe( ex({p,q},x=p+a*q and y=p+q and p^2+q^2 QEPCAD B (a,x,y,p,q) 3 (E p)(E q)[x=p+a q /\ y=p+q /\ p^2+q^2 Mathematica FullSimplify[Reduce[Exists[{p,q},x==p+a*q && y==p+q && p^2+q^2 この…

「２つの集合{x;0<x<a}，{x;b<x<1}が等しい」という式の入力，出力は，RedLogでは rlcad( all(x,0<x<a equiv b<x<1) ); a - b > 0 and a - 1 = 0 and b = 0 or a - b < 0 and a <= 0 and b - 1 >= 0 QEPCAD Bでは (a,b,x) 2 (A x)[ [ 0<x /\ x<a ] <==> [ b<x /\ x<1 ] ]. a - 1 <= 0 /\ b >= 0 /\ [ [ a - 1 = 0 /\ b = 0 ] \/ [ a <= 0 /\ b - 1 >= 0 …</x></x></x<a}，{x;b<x<1}が等しい」という式の入力，出力は，redlogでは>

同じ条件を (E x)(A y)[ 0 y^2 - 2 y >= m ] ]. と入力すると，QEPCADは a >= 0 /\ m + 1 >= 0 /\ m - a^2 + 2 a = 0 /\ m + 1 = 0 ] \/ [ a - 1 と答えます．

を合成すればより簡単な式が得られるだろうと期待しつつ，rlitab，rlgsn，rldnfの異なる２つ，異なる３つ，それぞれ６通りの合成をgに作用させたところ，２つの合成では，単独の場合と同様あまりぱっとしないrldnfが，３つの合成の一番最後の処理になると僅…

rlitab，rlgsn，rldnfを昨日の最小値の例，つまり procedure f(x)$x^2-2*x$ のもとでの g:=rlcad( ex(x,0=m) ); に作用させた結果を比較します．rlitab(g); a**2 - 2*a - m > 0 and a - 1 > 0 and m + 1 = 0 or a**2 - 2*a - m = 0 and (a - 1 = 0 and m + 1…

QE関数の出力は一般に複雑です．よって，式を簡約する関数，すなわち，simplifierの働きが重要になります．実数体コンテキストrにおいて利用できるsimplifierには・Standard Simplifier 常時適用されるrlsimpl・Tableau Simplifier タブロー法を採用したもの…

のもとでは，３つのQE関数rlqe，rlcad，rlhqeが使えることは既に述べました．これらは採用するQEの原理が異なり，同じ入力に対しても異なった挙動を示します． rlqeは，他の２つより一般に高速ですが，rlcadより結果の式は複雑です． rlcadは，rlqeより一般…

昨日の最後の結果は，例えば 0≦a≦1のときm=a^2-2a，1＜aのときm=-1 となりますが f1:=rlqe( ex(x,0=m) ); と入力すると，RedLogは f1 := m + 1 >= 0 and (a**2 - 2*a - m >= 0 and a - 1 >= 0 and (m + 1 = 0 or a**2 - 2*a - m > 0 and a - 1 = 0) or m = 0…

まず，関数fを procedure f(x) x^2-2*x と定義し，「aが関数fの値域に属する」という条件を rlqe( ex(x,f(x)=a) ); のようにQEすると，RedLogは a + 1 >= 0 と答えます．また，「点x=aにおいてf(x)が極小となる」という条件を rlqe( all(p,p>0 impl ex(q,q>0…

昨日の入力の説明です．まず load_package redlog; は文字通り，RedLog（reduce logic system）パッケージをロードするもので，MathematicaやmapleといったCASでも特定の内容を扱う際にはパッケージの明示的なロードが必要ですが，Reduceはその割合が大きい…

のまえに，Reduceでのお約束を少々．Reduceでは ・大文字，小文字に区別はありません． ・入力の終端は ; または $ で，後者を用いると結果を表示しません． ・先頭が n: の入力に対する結果は ws(n)，また直前の結果は ws でも参照できます（ws=work space…

まずReduce本体（windows版 http://sourceforge.net/projects/reduce-algebra/files/reduce-windows32-20101007.zip/download）をダウンロード，展開して出来たフォルダーにあるreduce.exeをダブルクリックすると，Reduce (Free CSL version)が起動します．…

パッケージかといえば，たとえば，a，bが実数のとき x^{2}+a x+b=0 となる正の数 x が存在する という条件を x を用いない形，すなわち a^{2}-4 b≧0 かつ（ a＜0 または b＜0 ） に同値変形することができます．

色々なものがある（数式処理システムの一覧 - Wikipedia）のですが，まずは，永い歴史を持ち，近年フリーとなったReduce（REDUCE (数式処理システム) - Wikipedia）の１階述語論理パッケージであるRedLog（http://redlog.dolzmann.de/）について，その使い方…

CAS（Computer Algebra System 数式処理システム - Wikipedia）について書いていこうと思います．