CAD の話が続きましたので，今回は QE のもう一つの基本，Virtual Substitution of Parametric Test Points をお話しましょう． 随分と長い名前というか，説明そのものですが，直訳なら「変数を含む試験点の仮想的代入」といった所でしょうか？ まぁ呼び方は…

今回は，Mathematica の CAD 関数についてのお話ですが，まずは用語の確認から，．．．，R^{n+1}(n≧1)の部分集合 X が Cylindrical であるとは，R^n の部分集合 Y と Y 上で定義された無限大を含めた実数値関数 f,g が存在して X={(x_1,...,x_n,x_{n+1}) ; (…

Maple 10 で登場した ChainTools パッケージに， Maple 14 で追加されたサブパッケージ SemiAlgebraicSetTools の目玉が，以前出力をご覧頂いた CylindricalAlgebraicDecompose です． この関数は，全空間を与えられた有限個の多項式関数の符号を変えない部…

前回紹介した RealRootClassification および RegularChains[ParametricSystemTools][BorderPolynomial], RegularChains[ParametricSystemTools][DiscriminantSequence], RegularChains[SemiAlgebraicSetTools][RealRootIsolate] with method='Discoverer' …

Maple 13 において，RegularChains のサブパッケージ ParametricSystemTools に加わった RealRootClassification 関数 （RegularChains[ParametricSystemTools] - Maple Programming Help）は，その名の通り，多項式で表された不等式制約を許す連立方程式の…

まず，RootFinding は，Isolate 関数のような方程式の数値解計算を主としたパッケージですが，Maple 12 で追加されたサブパッケージ Parametric は，不等式制約を許す連立方程式の open CAD（パラメータ＝自由変数空間の開集合による分解 http://www.sigsam.…

今回は，CAD は一回お休みして，いきなり始まった「 maxima で QE 」シリーズの１をお送りします． 以下では，∀x P(x) や ∃x P(x) (x∈R^N) のような量化子の種類が 1 で，しかも，自由変数を含まない論理式（閉論理式）を扱います． 閉論理式の真偽を判定す…

まず，前回の a 空間への射影 { a+3, a, a-1 } の各多項式の零点 -3，0，1 を境界として，実数全体 R を (-∞,-3)∪{-3}∪(-3,0)∪{0}∪(0,1)∪{1}∪(1,+∞) のように，7 個の部分集合に分解し，各部分集合，その式，その要素の一つ(sample point)を組にしたものを，…

これまでの考察により F(a,x) が a(∈R^n),x(∈R) についての実係数多項式 f_j(a,x) (j=1,...,M) を左辺，0 を右辺とする方程式や不等式を ∧ や ∨ で結合した論理式のとき ∃x F(a,x) や ∃x F(a,x) を満たす a 全体の集合を a についての実係数多項式 g_i(a) (i…

解集合の境界を含む可能性のあるものとして （１）もとの曲面達の共通部分の正射影 （２）もとの曲面の，正射影が含まれる空間に垂直な接平面の接点，および，特異点の正射影 があることを見ましたが，次の例ではどうでしょう？ ∃x ( 1≦x ∧ ax=1 ) QE 自体は…

前々回の例では，解集合の境界 {-3,1} は，直線と放物線の共通部分の y 軸への正射影 {-3,0,1} に含まれていましたが，例えば ∃x ( x≦a ∧ x^2-4x+a≦0 ) はどうでしょう？ QE は，直線 y=a と集合 x≦y ∧ x^2-4x+y≦0 との交わりが空でない（つまり，点を共有す…

前回の QE では，直線と放物線との共有点の y 軸への正射影を求めるため，実際に連立方程式を解きましたが，例えば のように次数が上がると，その実行は難しくなります．また のように変数の種類が増すと，n 次元空間の曲面どうしの共通部分は曲線または点（…

前回は解集合の図のみを正射影で求めるグラフィカルな QE でしたが，関数の種類，変数の個数が手頃であれば，同様の方法により，シンボリックに QE できます． 例えば (1) ∃x ( a≦x≦a+2 ∧ x^2-2 x+a≦0 ) を考えましょう．人間なら a について場合を分ける所…

前回，前々回のような解集合の図は，束縛・自由変数が合わせて 3 種類以下なら，与えられた論理式から簡単に求められます． 例えば，自由変数が 2 種類，束縛変数が 1 種類の特称量化論理式 を満たす点 とは，その点を通って 平面に垂直な直線上に を満たす…

前回の図を見ると，この解集合の境界は，どうやら2本の線分と謎の曲線とで構成されているようです． 線分については に対する の一部と推定できますが，いい感じに曲がった部分を見て，何とかそれを表す「式」を得られないかと思うのは自然な反応でしょう． …

今回は，凸，1 次式という条件を全て外し を満たす点 の集合（解集合） を についての連立 1 次不等式の表す集合（半代数集合）で内側から近似します（外側からは，前回と同じく， のサンプルを代入したものの連言を用います）．ここで， は の連結部分集合…

今回も ∀x ( x∈X → f(x)≧ax+b ) を満たす実数a，bの集合（解集合）を内と外から近似します． ただ，予告した下限，上限による適用範囲の広い評価の前に，特殊ではあるが精度の高い凸関数の 1 次式による近似を述べておきたいと思います． まず，外からの近似…

前回のような超越関数を含む論理式を QE する方法として，すぐ思いつくのは近似です． ここで言う近似とは，一般に述語論理の論理式は自由変数についての条件ですから，それを満たす点の集合をその部分集合（サブセット）と拡大集合（スーパーセット）で評価…

これまで幾度か述べたように現在の QE で扱える関数は原理上，代数関数（多項式を用いて定義できるもの）なのですが，驚くべきことに Mathematica は Reduce[ Exists[x,Sin[2*x]-Sin[x]==a],Reals ] Reduce[ ForAll[x,Exp[2*x]-Exp[x]>=a],Reals ] などの処…

処理が重いなら WorkingPrecision オプションを Infinity から有限に変更する手もありますが，それは Mathematica 固有の解決策なので，ここでは一般的な方法を採ります．すなわち Numeric に推定して，Symbolic に証明する という道です． 具体的には g[r_]…