2 定理の例

2.1 prover+に投げる

prover+ は(一階言語の)Thmを受け取るとProver語に変換してProver9に投げます。最初のThmを作ってみます。
\(\top\) \(\blacktriangleleft\) O
ソース67行目を見ると、このThmの査読では \(\top\) ◁ O が prover+ に投げられるハズと分かります。
実際に下の右側の「査読」ボタンを押してみて！ 2.1-1（2.1節の1番目のThmという意味）の右の方に「OK」と出てくるはず。
OK をクリックすると「Prover9が length:2 の証明を見つけた」事が分かり、さらに 〇 をクリックすると prover+ や Prover9 に投げられたものが確認できます。

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
ソース75行目では変数goalが使われています。「Thmのgoal」が自動的に代入されます。
査読をさせてみると、今度は length:5 の証明が見つかります。

2.2 vampire+に投げる

vampire+ は(一階{s,c}ソート語の)Thmを受け取るとTFF形式に変換してVampireに投げます。
上のThmに違うprfを付けてみます(ソースの83,85行目)。Vampireでlengthが4,28の証明が見つかります。
\(\top\) \(\blacktriangleleft\) O
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
このような簡単な問題では差が出ませんが、難しい問題ではProver9とVampireで得意・不得意が出てきます。

2.3 satallax+に投げる

satallax+ は高階言語のThmを受け取るとTHF形式に変換してSatallaxに投げます。
\(\top\) \(\blacktriangleleft\) O
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
Satallax は常に高階の証明探索をするので、一階の内容では Prover9・Vampire より時間がかかることが多いです。

2.4 hyperionにも投げる

長い証明ではprfを段に分けて書きます。ソース100行目では途中式変形まで書いてみました。Le1 <- … -| … という書法を使っています。
hyperion は証明探索をせず、それまででOKになったThmを決まった規則（合成・slash の除去・∀導入など）でつなぎ、Thm の形に組み立てます。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則

2.5 引っ掛かりやすい例

次のThmはきちんと査読が通ります。
\({\perp}\) \(\blacktriangleleft\) \(x \neq y\)
これは一階論理の性質です（sosからは \(x \neq x\) が出ます）。
査読は「書いた通り」に行われます。「相異なる2つの x, y」のつもりでもそうはなりません（自由変数は全称で閉じて読むので、sos は「すべての x, y について x ≠ y」です）。
ソース105行目にある上のprfの査読では、査読器が \({\perp}\) ◁ \(\neg ( x = y )\) を prover+ に投げ、それがProver9にテキストを投げ length:2 の証明が見つかっています。
ある相異なる2つについて述べたいときは、定数で \(\mathrm{a} \neq \mathrm{b}\) と書きます（\({\perp}\) ◀ \(\mathrm{a} \neq \mathrm{b}\) は通りません）。
あなたが査読器に疑念を抱いたなら、それは正しい姿勢でしょう。その健全性は最重要視されるものです。

2.6 一階論理で解ける高階論理

v^-Form などは高階変数です。それらを含むThm \(\mathcal{T}\) に対し、\(P\) を \(\mathrm{P}\) に置き替えるなどして、定数化したThmを \(\mathcal{T}\)|v-elim とします。
prover+・vampire+は高階変数を含むときは、まず |v-elim をすることで、\(\mathbb{L}_{\rm H}\)・\(\mathbb{L}_{\rm Hsc}\) も一部判定します。
\({\perp} \Rightarrow P\) \(\blacktriangleleft\) O
|v-elim をすると \({\perp} \Rightarrow \mathrm{P}\) ◀ O。
なお、こうして示せたことは、\(P\) に具体的な式を代入してよいことを意味しません（\(P\) は \(x\) などに依らない1つの命題です）。