Thm
Mathelは一階言語に翻訳されると、長ーくなりがちです。
しかし一階言語では一階論理が使えます。
一階言語に翻訳された上で「\({\tt X}\)が\({\mathcal A}\)から推論される」ことを \({\tt X}\) ◀ \({\mathcal A}\) と表します。
この形のものをThm、\({\tt X}\)をgoal、\({\mathcal A}\)をsosと言います。
その最終段階はProver9（一階論理による推論ができる無償ソフト）に委ねられます。
Thmの各Formが、一階言語に翻訳され、さらにProver9の言語に翻訳され、Prover9に送られます。
Prover9からの返答はoracleと呼ばれ、会員は◀をクリックすると見れます。\(\dagger\)
prep
「私たちにとって」は証明＝prepです。
良いprepを見つけProver9の探索空間を小さくすることを目標にします。
証明の能力を上げる＝prepの戦略を磨く、ことが重要課題です。
prepにもいろいろな手段を用意する必要がありますね？
W.から\0.を選び出すようなことだけでは全くたりません。
人間も「〇〇を一つとって固定する」や補題の利用など様々なことをします。
ruleとslash
よく使われるprep手段にslash計算があります。
これも機械にとっては容易に高速に実行できるものです。
終わりに
数学は記号列を変形していくゲームです。
これで最低限のルールが分かったと思いますので、ぜひライブラリをご覧下さい！
ライブラリでは記号や変換規則や定理などを蓄積しています。
なおライブラリでは、記述は淡々と行われ、記号の意味や読み方を与えたり親切に説明をすること等は基本的にありません。
私たちは会員を募集しています。
ルールの詳細などの私たちの発明の核心的な部分は非公開です。ぜひ会員になって共に議論しましょう！
代表：須田智彦[t@mshk1201.com]まで。