A Fully Automatic Theorem Prover with Human-Style Output https://link.springer.com/article/10.1007%2Fs10817-016-9377-1 既存の自動証明器と違って検証や効率ではなく、人間らしい証明出力の生成をゴールとした自動証明器の話。

導出原理(resolution)による証明は低レベル過ぎるとか、高水準な論理の道筋とか、記法などのconventionの活用の話は理解できるのだけれど、一方で自然言語として数学者にとって自然にみえるかどうかみたいな話は、個人的にはどうでも良いなぁ、と感じてしまう。

結果のタクティック集合の中身とその適用順位などは興味深い。 バックトラックせずに適用順位に従ってひたすら適用するだけというのは思い切った割り切りだけど、それでも簡単な定理は証明できるんだなぁ。 結果のテキスト生成はdeterministicにやっているので、特徴的なパターンは出てしまうけれど、 それ以外は割と人間っぽいかも。

実装はHaskellで3300行程度。 オリジナルの実装は https://github.com/mg262/research/raw/master/robotone.zip にあるけれど、最近の環境で試すならforkされた https://github.com/EdAyers/Robotone を試したほうが良いかも。