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) に可能な…