6 {s,c}ソートのThmを prover+ に投げる（参考）

6.1 多ソートとソート無しの論理

各ソート a について、元の言語に無い一項述語 :a を新しく作ります。
\({}^{*}\) を相対化とします … x のソートが a のとき ∀ x P は ∀ x (x:a ⟹ P) に、∃ x P は ∃ x (x:a and P) にします。
定理　多ソート言語の文 \({\tt P}\) と、文の集まり \(\Gamma\) について
　\(\Gamma\) から \({\tt P}\) が推論できる（多ソート）　\(\Longleftrightarrow\)　Ax と \(\Gamma^{*}\) から \({\tt P}^{*}\) が推論できる（ソート無し）
Ax は 各ソートは空でないこと（∃ x (x:a)）と、記号の型付け（f のgramが (a,b) なら x:a ⟹ fx:b） です。

6.2 一階翻訳

一階{s,c}ソート言語の Thm の一階翻訳とは「全称量化し、相対化して、Ax を添えた一階言語の Thm」です。全称量化 … \(x\) が自由に出現していれば \(\forall x\) 、\(X\) が自由に出現していれば \(\forall X\) を先頭につけます。
Ax は実際に出てくるソートと記号についてだけ添えます。ソートが互いに素であることは添えません。
◀ … p; の段では prover+ はまず一階翻訳をします。section1 の最後の Thm（1.3-3・goal ◀ +結合則 p;）では
　 \(\forall x \forall y \forall z \forall w \, ( x \mathbin{:}\mathrm{s} , y \mathbin{:}\mathrm{s} , z \mathbin{:}\mathrm{s} , w \mathbin{:}\mathrm{s} \Longrightarrow x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w )\)
　◁ \(\exists x \, ( x \mathbin{:}\mathrm{s} )\) ， \(\forall x \forall y \, ( x \mathbin{:}\mathrm{s} , y \mathbin{:}\mathrm{s} \Longrightarrow x + y \mathbin{:}\mathrm{s} )\) ， \(\forall x \forall y \forall z \, ( x \mathbin{:}\mathrm{s} , y \mathbin{:}\mathrm{s} , z \mathbin{:}\mathrm{s} \Longrightarrow x + ( y + z ) = ( x + y ) + z )\)
となり、これが Prover9 の入力です。

7 高階変数の定数化

v^-Form, ?v-Form などが高階変数です。それらを含む Thm \(\mathcal{T}\) に対し、\(P\) を \(\mathrm{P}\) に置き替えるなどして定数化した Thm を \(\mathcal{T}\)|v-elim とします。置き換える word はもとの Thm に無いものから選び、異なる高階変数は異なる word に、同じ高階変数は goal・sos を通じて同じ word に置き換えます。
\(\mathcal{T}\)|v-elim が一階言語の Thm になるなら、置き換え先の選び方によらず 　\(\mathcal{T}\) holds in \(\mathbb{L}_{\rm H}\) \(\Longleftrightarrow\) \(\mathcal{T}\)|v-elim holds in \(\mathbb{L}_1\)
これは一階論理の「解釈を決めていない記号について示せたことは、その記号を何にしても成り立つ」という事実によります。
prover+・vampire+ は高階変数を含むときは、まず |v-elim をすることで、\(\mathbb{L}_{\rm H}\)・\(\mathbb{L}_{\rm Hsc}\) も一部判定します。
\({\perp} \Rightarrow P\) \(\blacktriangleleft\) O
ソースで書くと ⊥ ⇒ P^ ◀ O を |v-elim すると ⊥ ⇒ |P^ ◀ O です（表示では P と |P の区別が斜体と立体だけ）。-| … p; でも通ります。
\(P\) \(\blacktriangleleft\) \(P\)
同じ高階変数は goal・sos を通じて同じ word に置き換えるので、P^ ◀ P^ は |P^ ◀ |P^ になり、示せます（別々の word にすると示せない）。sos には prop 名のほか、バッククォートの式を直接書けます。