ehito さん プロフィール

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

ehito さんのブログ記事

  • REDUCE 更新
  • https://sourceforge.net/projects/reduce-algebra/files/snapshot_2017-09-22 インストールスクリプト. svn co http://svn.code.sf.net/p/reduce-algebra/code/trunk reduce-algebra cd ./reduce-algebra ./configure --with-psl make sudo apt-get install libffi-dev ./ [続きを読む]
  • Wolfram Open Cloud
  • http://blog.wolfram.com/2016/01/28/launching-the-wolfram-open-cloud-open-access-to-the-wolfram-language/ で告知された通り,Wolfram Open Cloud として,Mathematica が https://sandbox.open.wolframcloud.com/ などで利用可能になっています. [続きを読む]
  • 実行例(5)
  • 入力は,主に http://www.cs.bath.ac.uk/~djw42/triangular/examplebank.pdf の Examples from [CMXY09](https://arxiv.org/pdf/0903.5221.pdf)から選びました. 環境は,Core i5-3210M 2.50GHz/8GB/Ubuntu 14.04/Maxima 5.40.0/SBCL 1.3.20 です. コントローラー qvpeds [続きを読む]
  • Lazard’s method(その1)
  • 1994年(Unpublished manuscript は 1990年)に Daniel Lazard が発表した(https://link.springer.com/chapter/10.1007/978-1-4612-2628-4_29)CAD の構成方法は,一般化された根の重複度(Lazard valuation)を保つ分割によるもので,その projection set(主係数,定数項 [続きを読む]
  • 結果の検証
  • 今回の 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)$ により,冪乗関数に変換して処理しています.流れを例示し
    ます. 次の式は恒真です [続きを読む]