今更だけれど、「人工頭脳「東ロボくん」、代ゼミ東大模試に挑戦　結果は“偏差値60”」 http://www.itmedia.co.jp/news/articles/1311/25/news121.html の答案例面白すぎる。 が、お前本当にTarskiの量化子除去アルゴリズム使っているのかと問い詰めたい。 二重指数程度の計算量で済む高速なCAD(Cylindrical Algebraic Decomposition)系のアルゴリズムとかでなく、ELEMENTARYでない(多重指数で抑えられない)Tarskiのオリジナルのアルゴリズムを本当に使ってるのかよ。 お前Tarski言いたいだけちゃうんのか、と。

それはそれとして、量化子除去に関して「変形の過程が長いため、計算紙で別途提出する」とあるけれど、これって proof term をちゃんと生成する量化子除去を実装しているということだと思うので、偉いなぁと思う。

あと、昨年の第二回「範疇文法と証明論」シンポジウム http://researchmap.jp/joadanh3a-8286/#_8286 の際にの発表「大学入試における「論理」とは？」で、組合せ範疇文法（CCG）使ってると言っていたような気がするけど、この数学の問題とかもCCGによる構文解析・意味解析で十分な精度が出ているということかな。（あまり記憶がはっきりしていないので、CCG使ってるというのは数学でない教科の話だったかも知れない……）