公開された東ロボくんの答案の論理式についての解説にもニーズがありそうなので今日はそれを書くことにします．まずは問題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/