6. 結論と展望
本稿では，「機械によって数学問題を解く」という行為を (1)
問題文の ZF の式への翻訳，(2) ZF の式から現実的に機械に
よる推論が可能な体系 (RCF++PA) の式への変換，(3) 「解
けている」と認められる項・式を得るための推論の実行，とい
う流れとして明確化し，これに基づく解答システムについて
(1) の自然言語処理のステップを中心に概説した．言語処理部
について理想化した実験設定ではあるが，RCF-QE ソルバー
を用いてテストデータの約 7 割に現段階で正答が得られたこ
とは，上記の方針について明るい見通しを与えるものである．
https://kaigi.org/jsai/webprogram/2013/pdf/622.pdf