三角形の内接円を一般化して 与えられた平面図形 D に含まれる円の半径 r の範囲 を考えます． そのような r の条件は r≧0 ∧ ∃(a,b)∀(x,y)( (x-a)^2+(y-b)^2≦r^2 → (x,y)∈D ) ですから，Mathematica の場合，D の条件を f として Reduce[ r >= 0 && Exists[{…

今回は現在の QE の問題点とその解決に向けた動きをお話します． 実際に QE プログラムを使った人が共通に感じるのは，やはりスペックの低さでしょう．これまで散々美味しいことを書いておきながら今更ですか！と叱られそうですが，少し複雑な処理になると，…

R^2 の部分集合 A が凸集合であるとは ∀a,b( a,b∈A → ∀s,t( s a + t b ∈ A ) ) となることであり，R^2 の部分集合 X を含む最小の凸集合，すなわち，X を含むすべての凸集合（少なくとも全空間は存在する）の交わりを C(X) で表すとき x ∈ C(X) ⇔ ∃s,t,u,p,q…

前回の最後に挙げたような条件の処理に適した「点（リスト）の個数を規定する量化子」いわゆる「Numerical Existential Quantifier」を作ることは比較的容易です． 例えば，一般に条件 P を満たす異なるリスト X が少なくとも k 個存在するという式を F(k,X,…

RedLog や Mathematica の量化子は変数のリストを束縛することが可能で，これまでも ex ( {x,y} , x^2+y^2=2 and x+y=a ); のような例を数多く扱ってきましたが，実際に入力すれば，直ちに ex(x,ex(y,a - x - y = 0 and x**2 + y**2 - 2 = 0))$ となることか…

ブログを読み返してみて，QEPACD B の特徴の一つである量化子の拡張について殆ど述べていないことに気付きました． QEPCAD B には，特称量化子 E，全称量化子 A の他に F = "for infinitely many" G = "for all but finitely many" C = "for a connected sub…

と言えば，やはり不等式の成立です．すなわち 変数が仮定を満たすならば，結論の不等式が成り立つ という論理式を QE すれば，その式と同値で量化子を含まない式（とくに，成り立つときは true，成り立たないときは false）が得られる（RedLog ではtrue，fal…

今回は極限のお話です． よく知られた CAS（計算機代数システム）には極限を求めるコマンドが実装されており，例えば を得るには，Reduce では limit( 1/x , x , a ) ; Mathematica では Limit[ 1/x , x -> a ] Maple では limit( 1/x , x = a ) ; maxima で…

今回も線形代数の話題です． 2 次の正方行列 が を満たすならばスカラー が存在して となるための の条件を考えます． まず行列を A:={{a,b},{c,d}};X:={{x,y},{z,w}};E2:={{1,0},{0,1}};O2:={{0,0},{0,0}}; のように準備し，それらについての等式を Logical…

今回は線形代数のお話です．係数，数ベクトルの成分は実数とします． まず，線形独立な 2 個の 2 項数ベクトルが存在することを見ましょう．数ベクトル(a,b),(c,d)が線形独立であるとは ∀s ∀t ( s(a,b) + t(c,d) = (0,0) → s=t=0 ) ということでしたから Red…

前回は最大値を求めるところを，値域まで求めてしまいましたので，今回は関数の最大値のみを求めます．と言っても方法はいつもと同じで，定義を論理式で表し，QE するだけです． まず最大値の定義ですが，集合 A を定義域とする実数値関数 f の最大値が M で…

今回は「問題を解く」とはどういうことなのかを QE の立場から見てみます． xy 平面上の楕円 x^2+3y^2=4 と直線 x+3y=k が異なる 2 点 A，B で交わるとき，3 角形 ABC の面積を S とおく．ただし，C(1，1) とする． このとき，S を k を用いて表し，S が最大…

今回は QE の立場から「代入」を考えます． よく知られた CAS（計算機代数システム）には代入のコマンドが実装されており，例えば，y=x^3+x^2 の x に 2 を代入した式を得るには，Reduce では sub( x=1 , y=x^3+x^2 ); Mathematica では ReplaceAll[ y==x^3+…

最新版の最新たる部分を見てみましょう．端末より reduce -w -b と入力すると のように Reduce の最新バージョン(20110414)が起動します．そこで一階述語論理パッケージ RedLog のサブパッケージある QEPCAD を load qepcad; とロードします（RedLog 単独で…

OS の準備ができたら，画面下のパネルにある地球のアイコンをクリックして，ウェッブブラウザを起動し，このページにアクセスしてください． そして次をコピーします．## ここからコピー sudo cp -f /etc/apt/sources.list.math /etc/apt/sources.list sudo …

http://www.math.kobe-u.ac.jp/vmkm/2011vm-info/knxm2011-on-vmware-player/index.html を参考に KNOPPIX/Math 2011 をインストールしておいてください． このブログでは，その OS 上に最新版の Reduce，QEPCAD B などを導入するスクリプトを提供し，それら…

更新をサボっている間に，ここで紹介したソフトの多くがバージョンアップしてしまいました． よって，最新版に対応した記事を近日中に公開することにします．