ehito さん プロフィール

  •  
ehitoさん: ATPとCASのこと
ハンドル名ehito さん
ブログタイトルATPとCASのこと
ブログURLhttp://d.hatena.ne.jp/ehito/
サイト紹介文ATP(自動定理証明)とCAS(計算機代数系)について書いていこうと思います.
参加カテゴリー
更新頻度(1年)情報提供32回 / 365日(平均0.6回/週) - 参加 2011/01/12 11:32

ehito さんのブログ記事

  • 結果の検証
  • 今回の QE ツールにおける入出力(に対応した論理式)の等価性の検証は,いつもお世話になっている qepmax(https://github.com/YasuakiHonda/qepmax)を介して QEPCAD B で行なっています.具体的には,次のように出力のリストを論理結合に変換するための関数 F2G を通した [続きを読む]
  • 実行例(4)
  • (%i1) (qvpeds ([],[a,b,c,d],0,h1,r11,0 ), qe( bfpcad(ext( '( a^3+b^2-1=0 and b^3+c^2-1=0 and c^3+d^2-1=0 and d^3+a^2-1=0 ) ))
    ) ); Evaluation took 14.3200 seconds (16.7700 elapsed) using 2101.559 MB. (%o1) [[a = root(a,1),b = root(b^2+ [続きを読む]
  • 近接根の識別
  • 仮に r, R を先の条件を満たすようにとるとして,そも,R をどのように定めるのか?という問題があります. 確かに,数値解の精度 R の系において,互いの距離が 2*R 以下である数値解を全て集めれば,重根に対する数値解は必ずそれに属します.しかし,互いの距離が 4*R 以 [続きを読む]
  • projection set に対する数値解の誤差(その1)
  • 単根に対する数値ソルバーの精度 r と数値解を係数に代入した方程式系の数値解の精度 R との関係を考えると ・数値解の代入による係数の摂動は Taylor の定理により r 程度. ・(前述のように)係数の摂動 r に対する厳密 n 重根の摂動は r^{1/n} 程度. なので,例えば, [続きを読む]
  • 重根に対する数値解の誤差
  • 先の出力の dist は,同じ値に対すると見做した数値解間の複素平面上での距離ですが,ソルバーの誤差 10^{-30} に対して,例えば,下の部分では 10^{-11} まで膨らんでいます. 1 multi-roots: (-6.24148303809758464007593708063b-13*%i)-6.38943104254668599198409918 [続きを読む]
  • QE on maxima
  • 以下は,現在作成中の QE ツールの出力例です. ・数値ソルバーの単根に対する精度は 10^{-fpprec}. ・2つの数値解間の距離が %ez より小ならばそれらは同じ値(重根や共通根)に対応し,%ez 以上ならばそれらは異なる値(近接根)に対応する数値解と見做しています. Max [続きを読む]
  • CAD on maxima
  • SARAG https://github.com/andrejv/maxima/tree/master/share/contrib/sarag が待ちきれない方のために作ってみました.ただし,lifting のネックである根の分離は realroots に任せ,符号判定も近似的です.また,例によって,コードの大半は結果の簡約に費やされています [続きを読む]
  • 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 seconds [続きを読む]
  • cineqs4 原理
  • cineqs4 は「真理値に関する中間値定理」により,原始式同士の結合の様子に立ち入ることなく,系を解いています.すなわち,... 一変数半代数系 F(x) と実数 a,b (a,<, [続きを読む]
  • 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)<=0 )); Evaluation took 0.0000 seconds (0.0000 elapsed) using 856 bytes. Evaluation took 0.0600 sec [続きを読む]
  • nns シリーズ更新
  • ・一変数半代数系の高速ソルバー cineqs2 の正式公開. ・solvex から呼ぶ不等式ソルバー sineq も一変数なら高速になりました(cineqs2 の一世代前のアルゴリズムなので少し遅いですが). load(qepmax)$ showtime:on$ display2d:false$ prtoff():=kill(prt)$ prton():=(pr [続きを読む]
  • 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) using 315.180 MB. ( [続きを読む]
  • 一変数半代数系の高速ソルバー cineqs2
  • 多変数半代数系のソルバーの基礎部分として作りました.かなり速いです. 以下のものは,パッケージのロードなしで動くように,真偽判定を簡素化,また,論理結合子も and, or になっています.なお,maxima の solve が虚数なのに %i を使わなかったり,実数なのに %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)$ defru
    le(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 乗とに対して  A(x^(a/b [続きを読む]
  • solvex 例
  • ソース http://d.hatena.ne.jp/ehito/20170106/1483705734 を見て戴くと判りますが,solvex には様々なスイッチがあり,説明が必要なのですが,それはまた後日とし(苦),ここではまずどんなものが解けるのか?をご紹介します. 係数にパラメータを含む不等式. (%i1) solv [続きを読む]
  • 等価性
  • nns,nnss と同じく,qex,solvex の入力と出力とは等価,つまり,変数に任意の実数を代入したとき,それらの true,false は一致します. 例えば,sqrt を含む場合,定義:y=sqrt(x)⇔(y^2=x∧y>=0) により,x<0 のとき,y=sqrt(x) は false ですから,前回の最後の例 [続きを読む]
  • solvex 概要
  • solvex は半代数系を指定された変数についての1次式を原始式とする系に変換する関数です. 例えば,3数の相加平均と相乗平均とが一致する条件を得ようとしても,qex では... (%i1) qex(a>=0 %and b>=0 %and c>=0 %and (a*b*c)^(1/3)=(a+b+c)/3); E [続きを読む]