Maxima さん,勘弁してください.

1と2は特別なのでしょうか? k@k ~ $ rmaxima --init= Maxima 5.39.0 http://maxima.sourceforge.net using Lisp CMU Common Lisp 21b (21B Unicode) Distributed under the GNU Public License. See the file COPYING. Dedicated to the memory of William …

cineqs4 更新

変更点 ・名前が cineqs4g になりました. ・処理の効率を改善.数パーセント高速化しましたが,下記の処理のため結果として遅くなりました(苦). (%i15) for c:1 thru 100 do (ep(0,0),cineqs4g('( x^3+abs(x+1)^(-1/4)-2>0 )))$ Evaluation took 5.2900 …

cineqs4 原理

cineqs4 は「真理値に関する中間値定理」により,原始式同士の結合の様子に立ち入ることなく,系を解いています.すなわち,... 一変数半代数系 F(x) と実数 a,b (a,=, 例えば,f(a)>0はtrue,f(b)>0はfales(つまり,f(b) ⇒F(x) のある原始式 rel(f(x),…

cineqs4 使用例

作動確認バージョン. Maxima 5.39.0 using Lisp CMU Common Lisp 21b (21B Unicode) 高次不等式. (%i1) ep(1,0)$cineqs4('( (x-1)*(x^2-2)*(x^3-3)*(x^2+4)<=0 )); Evaluation took 0.0000 seconds (0.0000 elapsed) using 856 bytes. Evaluation took 0.0…

一変数有理冪半代数系ソルバー cineqs4

cineqs2 を分数関数や有理冪乗(fractional power)関数で表された方程式,不等式まで扱えるように拡張しました. コードの大半は,Maxima の非論理的挙動を封じるためのものです(笑). 作動確認は Maxima 5.39.0 on Ubuntu 及び windows で行っています.…

Maxima さん,bug ってますよ.

Maxima 5.39.0 http://maxima.sourceforge.net using Lisp CMU Common Lisp 21b (21B Unicode) Distributed under the GNU Public License. See the file COPYING. Dedicated to the memory of William Schelter. The function bug_report() provides bug re…

nns シリーズ更新

・一変数半代数系の高速ソルバー cineqs2 の正式公開. ・solvex から呼ぶ不等式ソルバー sineq も一変数なら高速になりました(cineqs2 の一世代前のアルゴリズムなので少し遅いですが). load(qepmax)$ showtime:on$ display2d:false$ prtoff():=kill(prt…

solvex 原理

solvex の処理手順は,人間が計算機を用いて解く場合と同じです.すなわち,...(ステップ1)presimp,つまり,入力を qex で半代数系に変換 (オプションスイッチ)presimp:l で qex ではなく,p2t を通さない簡約 lineq を利用.sqrt が係数のみに現れ…

toy problems

最後の簡約は重いので無効化します(笑). (%i1) postsimp:off$ Evaluation took 0.0000 seconds (0.0000 elapsed) using 32 bytes. 放物線と直線との交わり. (%i2) solvex(y=x^2 %and x+y=1,x,y); Evaluation took 5.4600 seconds (11.3400 elapsed) usin…

一変数半代数系の高速ソルバー cineqs2

多変数半代数系のソルバーの基礎部分として作りました.かなり速いです.以下のものは,パッケージのロードなしで動くように,真偽判定を簡素化,また,論理結合子も and, or になっています.なお,maxima の solve が,虚数なのに %i を使わなかったり,実…

qex 原理(その2)

p2t では abs,max2,min2 も defrule(powertk2, abs(aa), (aa^2)^(1/2))$ defrule(powertk3, max2(aa,bb), (aa+bb+abs(aa-bb))/2)$ defrule(powertk4, min2(aa,bb), (aa+bb-abs(aa-bb))/2)$ により,冪乗関数に変換して処理しています.流れを例示します.次…

qex 原理(その1)

qex は入力を関数 p2t を通して,qe に渡すだけの関数なので,以下は,p2t のお話です.p2t (rational power to Tarski) とは,有理数乗を含む入力を特称量化することで多項式による系に変換する関数で,その原理は,原始式 A と x の既約分数 a/b 乗とに対…

solvex 例

ソース http://d.hatena.ne.jp/ehito/20170106/1483705734 を見て戴くと判りますが,solvex には様々なスイッチがあり,説明が必要なのですが,それはまた後日とし(苦),ここではまずどんなものが解けるのか?をご紹介します.係数にパラメータを含む不等…

等価性

nns,nnss と同じく,qex,solvex の入力と出力とは等価,つまり,変数に任意の実数を代入したとき,それらの true,false は一致します.例えば,sqrt を含む場合,定義:y=sqrt(x)⇔(y^2=x∧y>=0) により,x-1] ],出力:[ [a システム自身に等価性をチェックさ…

solvex 概要

solvex は冪乗根関数で表された方程式,不等式の系を指定された変数についての1次式を原始式とする系に変換する関数です.例えば,3数の相加平均と相乗平均とが一致する条件を得ようとしても,qex では... (%i1) qex(a>=0 %and b>=0 %and c>=0 %and (a*…

qex 概要

以下は Maxima 5.39.0 using Lisp CMU Common Lisp 21b (21B Unicode) 上での実行です.qex は qe コマンドを有理数冪入力対応に拡張したもの(qe extended version)であり,qex([],formula) は qex(formula) のように省略可能です.また,出力は qe と同じ…

nns シリーズ更新

新規の関数 ・qex qeの拡張版,有理数冪の入力に対応. ・solvex 多変数の方程式,不等式を原始式とする quantifier free な論理式の solver,有理数冪の入力,出力に対応. /* 17.01.09.Mon. 07:50:51 */ load(qepmax)$ showtime:on$ display2d:false$ prt(…

ncond 動かない式を動かす

以前にも述べましたが,変数の個数を低減させた必要条件を付加する ncond は強力で,nnss,nnsolvexx の求解能力はこの関数によるヒントの賜物とも言えます. (%i98) f:(a^2+b^2+c^2<=3)%and(a*b*c>=1)$ Evaluation took 0.0100 seconds (0.0200 elapsed) us…

nnssdn 二重否定の利用

次の不等式を簡約します. (%i90) f:x^3+y^3+z^3>=3*x*y*z; Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.859 KB. (%o90) z^3+y^3+x^3 >= 3*x*y*z まずは,qepmax から.... (%i91) qe([],f); Evaluation took 0.0800 seconds (0.2700 elaps…

nnss 見易い式を求めて

次の不等式を簡約します. (%i86) f:(x^2-1)*(x^2-4)*(x^2-9)<0; Evaluation took 0.0000 seconds (0.0000 elapsed) using 1.344 KB. (%o86) (x^2-9)*(x^2-4)*(x^2-1) < 0 まずは,qepmax + nns です.悪くはありませんが,ちょっと解り難いですね. (%i87) …

dnf から cnf へ

式の簡約は,まず選言形に直し,得られた連言項毎に処理するのが基本です.よって結果は (%i70) qe([],(a^2=1)%and(b^2=1)); Evaluation took 0.3400 seconds (0.5200 elapsed) using 12.210 MB. (%o70) (a-1 <= 0) %and (a+1 >= 0) %and (((a-1 = 0) %and (…

nns シリーズ

maxima 上の QE パッケージである qepmax の周辺関数を幾つか公開します.各関数の入力と出力とは等価な式です.・dnf,cnf 選言,連言形に変換 ・ncond 変数の個数の低減(大規模な式も扱えるように map から for ループに変更しました) ・nns,nnscan,nnsca…

LK の健全性の証明

各シグネチャーから得られる任意の論理式は,証明論においては,証明系で証明できる式,すなわち,定理式か否かに,モデル論においては,任意の構造,任意の変数への個体割り当てに対して真となる式,すなわち,恒真式か否かに,それぞれ分類されますが,そ…

「開いた式」

「開いた式」とは「変数の自由出現(あるいは自由変数)を含む論理式」のことで,その真理値の定め方には幾つかの立場があります.言語,構造を固定した上で,伝統的(?)なのは,変数への個体割り当てを用いて立場1 割り当て毎に真偽を与える立場2 割り…

Empty domain

古典的(?)な一階の古典論理の意味論では,ドメインAは空でないとされ,その理由として,Aが空では,∀x.p(x),つまり「任意のxについて,x∈Aならばp(x)」が真,∃x.p(x)つまり「あるxについて,x∈Aかつp(x)」が偽,したがって,定理式 ∀x.p(x)→∃x.p(x) が偽…

PVSの使い方

今更ですが,使い方です.端末から pvs とすると,emacsが起動し M-x nf でNew file name:と尋ねられ,例えばdemoe20160519と適当に入力すれば,demo20160519.pvsが demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % END…

skeep

PVSのskeepコマンドは,本来は x!1 などのように新規に導入すべきスコーレム定数を,衝突がない限り束縛されていた変数と同じ名前で導入してくれます. f1 : |------- {1} (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) => (EXISTS (x: A): (p(x) AN…

HOL Light vs PVS (3)

g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o …

計算機は囁く

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

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 5.37.0, wxMaxima 15.08.0

公開されました. 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 <…

fourier_elim を懐柔する(その2)

前回の 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 …

fourier_elim を懐柔する

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)))…

動かない式を動かす(nnsolve その4)

まず,次をご覧ください. (%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 とともに(nnsolve その3)

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

dnf と cnf(nnsolve その2)

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

nnsolve その1

原理は単純で,入力 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) のように簡約…

nnscan

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…

clisp,sbcl,cmucl

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…

qepmax

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

JAPE

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

選言から連言へ

ちょっとした経緯があり,NK,LKにおけるド・モルガン則の証明の作成手順を述べます.ド・モルガン則は,¬(〇*□)⇔(●・■)の形の定理(〇は●の否定,■は■の否定,*,・の一方は,∨他方は∧)であり,証明は¬(〇*□)⊢(●・■)と(●・■)⊢¬(〇*□…

選言から連言へ

ちょっとした経緯があり,NK,LKにおけるド・モルガン則の証明の作成手順を述べます.ド・モルガン則は,¬(〇*□)⇔(●・■)の形の定理(〇は●の否定,■は■の否定,*,・の一方は,∨他方は∧)であり,証明は¬(〇*□)⊢(●・■)と(●・■)⊢¬(〇*□)…

Algorithms for Trigonometric Curves (Simplifcation,Implicitization,Parameterization)

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[…

Algorithms for Trigonometric Curves

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,…