SyNRAC の岩根秀直さん（富士通研究所）のサイト https://github.com/hiwane/qe_problems/blob/master/problems/exam/manual-fof/tsukuba2010-Ri-1-m.mpl他の QE ツールの出力との比較 http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/2019-…

．．．とは言え，sep の評価なしでは，いくら R を小さくしても，前回の冒頭で述べたように，近接根に対応した数値解をカウントしてしまう可能性を排除出来ないかのように見えます．しかし，我々が扱うのは一般の系ではなく，CAD の projection set であり，…

さて，r, R を先の条件を満たすようにとるとして，そも，R をどのように定めるのか？という問題があります．確かに，数値解の誤差 R の系において，互いの距離が 2*R 以下である数値解を全て集めれば，重根に対する数値解は必ずそれに属します．しかし，互い…

誤差 r の数値解を係数に代入した方程式系の数値解の誤差 R との関係を考えると・数値解の代入による係数の摂動は Taylor の定理により r 程度． ・係数の摂動 r に対する厳密 n 重根の摂動は同じく r^{1/n} 程度．なので，例えば，前回の 4096*c^3+27*b^4（…

先の出力の dist は，同じ値に対すると見做した数値解間の複素平面上での距離ですが，単根の場合の（絶対）誤差 10^{-30} に対して，例えば，下の部分では 10^{-11} まで膨らんでいます． 1 multi-roots: (-6.2414826969557199979633340867b-13*%i)-6.389431…

以下は，現在作成中の QE ツールの出力例です． ・有効桁数が fpprec の多倍長浮動小数点数を使用． ・２つの数値解間の距離が %ez より小ならばそれらは同じ値の根（重根や共通根）に対応し，%ez 以上ならばそれらは異なる値の根に対応する数値解と見做して…

SARAG https://github.com/andrejv/maxima/tree/master/share/contrib/sarag を待ちきれない方のために作ってみました．ただし，lifting のネックである根の分離は realroots に任せ，符号判定も近似的です．使用例（wxmaxima 等で実行すると見易いと思いま…

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 …

変更点 ・名前が 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 は「真理値に関する中間値定理」により，原始式同士の結合の様子に立ち入ることなく，系を解いています．すなわち，．．． 一変数半代数系 F(x) と実数 a，b (a,=, 例えば，f(a)>0はtrue，f(b)>0はfales（つまり，f(b) ⇒F(x) のある原始式 rel(f(x),…

作動確認バージョン． 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…

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

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…

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

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

最後の簡約は重いので無効化します（笑）． (%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…

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

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

ソース 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 は冪乗根関数で表された方程式，不等式の系を指定された変数についての１次式を原始式とする系に変換する関数です．例えば，３数の相加平均と相乗平均とが一致する条件を得ようとしても，qex では．．． (%i1) qex(a>=0 %and b>=0 %and c>=0 %and (a*…

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

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

以前にも述べましたが，変数の個数を低減させた必要条件を付加する 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…

次の不等式を簡約します． (%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…

次の不等式を簡約します． (%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) …

式の簡約は，まず選言形に直し，得られた連言項毎に処理するのが基本です．よって結果は (%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 (…

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

各言語の任意の論理式は，証明論においては，証明系で証明できる式，すなわち，定理式か否かに，モデル論においては，任意の構造，任意の変数への個体割り当てに対して真となる式，すなわち，恒真式か否かに，それぞれ分類されますが，その分類が同じ結果と…