Mathematica は当然 In[5]:= Reduce[Exists[x, 0 <= x <= 1 && y == x^2 - 2 a x], Reals] Out[5]= (a <= 0 && 0 <= y <= 1 - 2 a) || (0 < a <= 1/2 && -a^2 <= y <= 1 - 2 a) || (1/2 < a <= 1 && -a^2 <= y <= 0) || (a > 1 && 1 - 2 a <= y <= 0) と答え…

set_goal([`&0 < b pow 2 - &4 * a * c`],`?x. a * x pow 2 + b * x + c = &0`);; e(ASM_CASES_TAC `a = &0`);; e(ASM_CASES_TAC `b = &0`);; e( X_GET_TAC 0 );; e( ASM_SIMP_TAC [] );; e( ARITH_TAC );; e( EXISTS_TAC `-- c / b` );; e( ASM_REAL_FIELD_…

公開されました． Maxima -- GPL CAS based on DOE-MACSYMA - Browse Files at SourceForge.net wxMaxima - Browse /wxMaxima at SourceForge.net

g(`!n. 3 < n ==> 2 EXP n < FACT n`);; e(INDUCT_TAC);; e(ARITH_TAC);; e(SIMP_TAC[LT;EXP;FACT]);; e(STRIP_TAC);; e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);; e(MATCH_MP_TAC LESS_MULT);; e(ASM_ARITH_TAC);; prove (`!n. 3 < n ==> 2 EXP n <…

前回の qfq では，例えば (%i1) f:abs(x-a)=abs(x-b)+c; (%o1) abs(x - a) = abs(x - b) + c (%i2) qfq(f); (%o2) ((0 < c) %and (a = b - c) %and (x = b)) %or ((0 < c) %and (b = a - c) %and (x = a - c)) %or ((a = b) %and (c = 0) %and (x = b)) %or …

abs や max，min も気軽に使えるよう，fourier_elim を内蔵した fqe を作りました． f2q(f):=subst([universalset=true,emptyset=false,"or"="%or","["="%and"],f)$ qfq(f):=block([g], if op(f)="%and" then (g:args(f),f2q(fourier_elim(g,listofvars(g)))…

まず，次をご覧ください． (%i1) f:((x-1/x)^2+(y^2-4*y+5)^3+(z+1)^2/z^4<=1)%and(x<0); 2 (z + 1) 2 3 1 2 (%o1) (x < 0) %and (-------- + (y - 4 y + 5) + (x - -) <= 1) 4 x z 人間が見るとバレバレですが，ストレートな qepmax では (%i2) qe([],f); 2…

solve は非常に強力な関数で (%i1) solve(x=y,[x,y]); (%o1) [[x = %r1, y = %r1]] と解いてくれます（笑）．これを抑えるには (%i2) solve(x=y,[x,y]),linsolve_params:false; (%o2) [[x = y]] とすればよいのですが，次数が上がると，聞く耳を持たないご様…

選言標準形，連言標準形は代数で言えば，それぞれ展開，因数分解に当たる基本的なものであり，前者は所謂（排他的とは限らない）場合分けなので，方程式系の解の構成には欠かせません．その実装は簡単で，例えば，A ∧ (B ∨ C) を (A ∧ B) ∨ (A ∧ C) に可能な…

原理は単純で，入力 f を選言標準形 ∨_k f_k に直し，f_k を方程式系部分 p_k と，不等式・非等式系部分 q_k との連言 p_k ∧ q_k に分解，p_k を maxima の solve で処理した結果 r_k を用いて，∨_k (r_k ∧ q_k) を出力とするものです．実装において問題とな…

QEPCAD B，従って，qepmax では (%i1) qe([[A,x]],(x=1)%eq(x^2+a*x+b=0)); 2 (%o1) (a - 4 b = 0) %and (b + a + 1 = 0) (%i2) qe([[A,x]],(x^2+x=1)%implies(x^2+a*x=b^2)); 4 2 2 2 (%o2) (a - 1 = 0) %and (b + a b - 3 b - a + a + 1 = 0) のように簡約…

nns は最も外にある %and または %or に作用するのみなので (%i1) nns(((x>=0)%and(x=0))%or((x>=1)%and(x=1))); (%o1) ((x = 0) %and (x >= 0)) %or ((x = 1) %and (x >= 1)) (%i2) nns((((x>=0)%and(x=0))%or((x>=1)%and(x=1)))%and((y>=0)%and(y=0))); (%…

アルゴリズムを「簡約」し，コストを半減させました． nns(f):= block([cl,L,fk],cl(f,g):=length(f)<=length(g), L:sort(rest(full_listify(powerset(setify(args(f))))),cl), if op(f)="%and" then for k:1 thru length(L) do (fk:substpart("%and",part(L…

nnsの原理は冪集合によるものなので，式が少し長くなるとそれなりに時間が掛かります．ということで，Lispを替えて実行してみると．．． のように，速度，メモリのバランスはやはり cmucl が良さそうです．

QEPCAD B，従って，qepmax では (%i1) qe([],x^2=1); (%o1) (x - 1 <= 0) %and (x + 1 >= 0) %and ((x - 1 = 0) %or (x + 1 = 0)) (%i2) qe([[X2,x]],x^2+a*x+1=0); (%o2) (a - 2 # 0) %and (a + 2 # 0) %and ((a - 2 > 0) %or (a + 2 < 0)) のように簡約が…

Redlog，REDUCE のコードが更新されました．最新版の maxima（5.36.1），wxmaxima（15.04.0）も併せて書いておきます． mkdir ~/CAS (* WxWidget http://codelite.org/LiteEditor/WxWidgets30Binaries#toc2 *) (* resuce csl 及び wxmaxima には必要 *) sudo…

以前，mathlibre の wiki に書いたものです（wiki はサーバーのトラブルで最近の記事が消えています） *maxima からの利用 「qepmax」パッケージをロードすると，maxima 上から QEPCAD B が利用できます． 論理記号 %implies %replies %eq %or %and %neg A E…

*JAPE JAPE（Ｊ∀Ｐ∃）はユーザーが論理体系，理論をコード化し，証明図（Fitch diagrams，Gentzen trees）やcounter model（Kripke diagrams）を簡単なマウス操作により作成できるproof calculatorです． // - Japeカーネルにコード化の仕様（テキストファイ…

ちょっとした経緯があり，ＮＫ，ＬＫにおけるド・モルガン則の証明の作成手順を述べます．ド・モルガン則は，￢（〇＊□）⇔（●・■）の形の定理（〇は●の否定，■は■の否定，＊，・の一方は，∨他方は∧）であり，証明は￢（〇＊□）⊢（●・■）と（●・■）⊢￢（〇＊□…

ちょっとした経緯があり，ＮＫ，ＬＫにおけるド・モルガン則の証明の作成手順を述べます．ド・モルガン則は，¬（〇＊□）⇔（●・■）の形の定理（〇は●の否定，■は■の否定，＊，・の一方は，∨他方は∧）であり，証明は¬（〇＊□）⊢（●・■）と（●・■）⊢¬（〇＊□）…

H.HONG,J.SCHICHO.Jurnal of Symbolic Computation 26(1998),279-300. (* 次数 *) TrigDegree[ft_, t_] := Exponent[TrigToExp@ft, Exp[I t]]; (* 主係数 *) TrigLeadingCoefficient[ft_, t_] := Coefficient[TrigReduce@ft, Through[{Cos, Sin}[TrigDegree[…

TrigDegree[ft_, t_] := Exponent[TrigToExp@ft, Exp[I t]]; TrigLeadingCoefficient[ft_, t_] := Coefficient[TrigReduce@ft, Through[{Cos, Sin}[TrigDegree[ft, t] t]]]; TrigQuotientRemainder0[ft_, gt_, t_] := Block[{X = TrigLeadingCoefficient[ft,…

*JAPE JAPE（Ｊ∀Ｐ∃）はユーザーが論理体系，理論をコード化し，証明図（Fitch diagrams，Gentzen trees）やcounter model（Kripke diagrams）を簡単なマウス操作により作成できるproof calculatorです． // - Japeカーネルにコード化の仕様（テキストファイ…

以前，mathlibre の wiki に書いたものです（wiki はサーバーのトラブルで最近の記事が消えています） *maxima からの利用 「qepmax」パッケージをロードすると，maxima 上から QEPCAD B が利用できます． 論理記号 %implies %replies %eq %or %and %neg A E…