センター試験の ・２次関数の問題 ・（帰納的に構成された）数列の問題に対応しました．入力と出力の例を挙げます．2012数学ⅠＡ第２問 $a,\ b$を定数として2次関数 $$y=-x^2+(2a+4)x+b\ \cdots\ \textcircled{1}$$ について考える． 関数$\textcircled{1}$の…

数学のセンター試験はいわゆる空所補充，つまり，問題文自体が数学的な主張になっているものが殆どです．また，一部の並び順を除けは正解は一意的です．従って，その主張をMathematicaの流儀による論理式に書き換えさえすれば，後はループを用いて空欄に選択…

センター試験の自動解答へのアプローチには（A）二次試験と同じく自前で得た結果を設問の空欄に当てはめる（B）設問の空欄に全ての選択肢を当てはめたものから正しいものを見出すという２つが考えられます． （A）で不都合なのは途中経過，従って誘導部分の…

Isabelle2013-2 が公開されました．http://www.cl.cam.ac.uk/research/hvg/Isabelle/

突然（でもない？）ですが，日本語混じりの LaTeX の問題文を入力とする自動解答システムを試作しました．扱い易い問題ならそれなりに処理できるようになりましたので，これについて書いていこうと思います． 自動解答といっても QE を含めた数式処理は Math…

第３問です．http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zenki/ これも最小値の定義を適用し，minが設問の最小値に等しいという式を Mathematica に処理させるなら Reduce[Exists[{x,y},x^2 + y^2 <= 25&&2x + y<=5 , min== x^2 + y^2 - 2a x - 2b…

昨日の ca は書き下すと Sqrt[a^2+(Sqrt[2]+Sqrt[1+a^2])^2]+\[Sqrt](2+1/8 (-24 Sqrt[2]-(48 Sqrt[2])/a^2+(64 Sqrt[1+a^2])/a^2+(4 Sqrt[2] Sqrt[96+64 a^2-64 Sqrt[2] Sqrt[1+a^2]])/a^2-(4 Sqrt[1+a^2] Sqrt[96+64 a^2-64 Sqrt[2] Sqrt[1+a^2]])/a^2))^2…

http://d.hatena.ne.jp/ehito/20131208/1386496330 で述べた（４）は ∃k( ∃x(x∈D∧k=f(x)) ∧ ∀x(x∈D→k≦f(x)) ∧ ∀x(x∈D→k≧f(x)) ) であり，これはDが空集合でないなら（５），つまり ∃k( ∀x(x∈D→k≦f(x)) ∧ ∀x(x∈D→k≧f(x)) ) と等価です． しかも，∀x(x∈D→0≦p(x…

これまでの http://d.hatena.ne.jp/ehito/20131206 および http://d.hatena.ne.jp/ehito/20131208/1386469586 では，前回の（１）を利用した訳ですが，以下では（２），つまり，まず，その「定数」をaのサンプルに対する関数値として得た後，任意のaに対して…

（１）値域がシングルトンになる ∃c(∃x(x∈D→f(x)=c))（２）ある関数値と任意の関数値が等しい ∃x(x∈D∧∀y(y∈D→f(x)=f(y)))（３）任意の２つの関数値が等しい ∀x(∀y(x∈D∧y∈D→f(x)=f(y)))特に値域が全順序集合の場合，その（４）最大元と最小元とが等しい（５）…

http://code.google.com/p/mecab/ https://code.google.com/p/cabocha/ を使うとデフォルトでもこんなことが出来るんですね．．．私の知らない世界です．入力 aを正の定数とする．実数x,yが■を満たすとき，▲の最小値を求めよ． 出力 * 0 3D 0/1 1.651767 a …

現在のいわゆるSymbolic QEで扱えるのは原理的に多項式のみです（Mathematicaのような根号を受け付けてくれるものでも内部で書き直しています）． なら入力の時点から多項式にしておきましょう．という方針でやってみます．問題は http://www.yozemi.ac.jp/n…

大学入試程度しかもparametricでないなら，MinimalPolynomialを用いて根号内のQ上の共役を求め，和と積の値を取り出せばよい訳ですが，今回はaの値によってはSqrt[1+a^2]∈Qとなることもあり，この手は使えません． そこでメタレベル，つまり，Mathematicaの…

http://d.hatena.ne.jp/ehito/20131129/1385725290 に続き 人間が問題を訳した場合，計算機は本年の東大文科数学の問題をどの程度処理できるか？ の第２問です．http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zenki/ 出題テーマは「２次曲線の性質を…

ニュースの画像をあらためて観たのですが，東ロボくんはSyNRACに実装されているSNCADを使っていました．それは．．． http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CCoQFjAA&url=http%3A%2F%2Fgcoe-mi.jp%2Ftemp%2Fpublish…

東ロボくんが答案でその名を挙げていた表題のもの，最も初期のQEの結果ということで，関連した論文の歴史紹介では必ず触れられますが，現在主流のCAD(Cylindrical Algebraic Decomposition)やVS(Virtual Substitution)より複雑で，正直，Tarski(1948), A dec…

公開された東ロボくんの答案の論理式についての解説にもニーズがありそうなので今日はそれを書くことにします．まずは問題http://livedoor.blogimg.jp/hyonko1007/imgs/0/4/04cec153-s.jpg書き写すと aを正の定数とする．実数x,yが1/2≦x≦1,a≦y≦2aを満たすと…

第１問 全体としてのポイントは関数gを対応と捉える所です． まず，gのグラフに(t,u)が属する条件を求めます． 実際の問題文は幾何学的に表現されているので，機械での翻訳はかなり難しそう． In[1]:= G[t_, u_] := Reduce[Exists[{p, q}, ForAll[x, x*(x - …

東ロボくんの目標は東大文科合格らしいので，今回からしばらく 人間が問題を翻訳した場合，本年の東大文科数学の問題をどの程度処理できるのか？を試してみようと思います．問題と解答はこんな感じ．http://www.yozemi.ac.jp/nyushi/sokuho/recent/tokyo/zen…

旬のネタという事で少し．．．東ロボくんが式には書き直せたが，そこから進めなかったという東大プレ理系１番http://blog.livedoor.jp/hyonko1007/archives/29936831.htmlもし座標を用いたのであれば，そんな(7変数？の)QEは無謀です．ここは言語系の方に頑…

Isabelle2013-1 が公開されました． http://www.cl.cam.ac.uk/research/hvg/Isabelle/

勿論 echo 'thf(nat,type,nat : $tType). thf(z,type,z : nat). thf(suc,type,suc : nat > nat). thf(nat_induction,axiom,( ! [P : nat > $o] : (((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) => (! [N : nat] : (P @ N))) )). thf(f,type,f …

帰納法のユニファイもお任せです． echo 'thf(nat,type,nat : $tType). thf(z,type,z : nat). thf(suc,type,suc : nat > nat). thf(nat_induction,axiom,( ! [P : nat > $o] : (((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) => (! [N : nat] :…

という訳で，高階論理自動定理証明界のホープ Satallax の登場です． echo 'thf(type_x,type,x : $tType). thf(type_y,type,y : $tType). thf(f,type,f : x > y). thf(gl,conjecture, ((! [X1 : x, X2 : x] : (((f @ X1) = (f @ X2)) => (X1=X2))) <=> (? [G…

「高階論理の定理証明システム」という言葉がよく用いられ，実際，主なプルーフ・アシスタントでは高階論理の定理式が扱えます．しかし，それは関数や述語を変数のまま使えるということであり，高階の decision procedure を備えているという意味ではありま…

KeYmaera のいう hybrid system とは，自身の状態に応じて設定を変える系のことで，その性質を扱う論理を，差分で表された action が各変数を繰り返しの回数についての関数と見做すことに加え，微分で表された action が各変数を時間についての関数，従って…

KeYmaera が非線形方程式を解かずに結論を得る仕組みは \problem{ini->\[{ode}\]f>=g} に対して，まず，時刻 0 における成立 ini->f>=g を示し，さらに任意の非負の時刻における f'>=g' の成立を正規型の ode を用いてこの結果から導関数を消去，証明する素…

KnxmWiki には長所のような書き方をしましたが，外部のツールをバックエンドに用いることは，理論の公理的構成においては致命的です．それはかつて多くの証明系が惑わされた甘美な道ですが，バグを抱えたグラマラスな CAS と心中するのは願い下げなわけで．…

KeYmaera（キメラ）の目玉の一つは 微分方程式系，微分不等式系で表された Continuous evolution を action に使えること ですが，見ての通り \programVariab 以下で，ロジカルな変数が時間の関数なのか否かを明示していません．例えば，先の２つ目の例の時…

http://www.knoppix-math.org/wiki/index.php?KeYmaera に紹介記事を書きましたが，幾つか補足しておきます．差分方程式の例 \programVariables{R x;} \problem{x\[x:=x/2+1*\]x 微分方程式の例 \programVariables{R x,v,a;} \problem{x>=0&a>=0&(v>=0|(a>0&…