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…