・一変数半代数系の高速ソルバー 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(…