2 Examples of theorems

2.1 Throwing to prover+

When prover+ receives a Thm (of the first-order language), it converts it into the Prover language and throws it to Prover9. Let us make our first Thm.
\(\top\) \(\blacktriangleleft\) O
Looking at source line 67, you can tell that in the review of this Thm \(\top\) ◁ O should be thrown to prover+.
Actually press the "査読" (Review) button at the bottom right! "OK" should appear to the right of 2.1-1 (meaning the 1st Thm of section 2.1).
Clicking OK shows that "Prover9 found a proof of length:2", and further clicking 〇 lets you see what was thrown to prover+ and Prover9.

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
Source line 75 uses the variable goal. "The goal of the Thm" is substituted automatically.
If you have it reviewed, this time a proof of length:5 is found.

2.2 Throwing to vampire+

When vampire+ receives a Thm (of the first-order {s,c}-sorted language), it converts it into TFF format and throws it to Vampire.
Let us attach different prfs to the Thms above (source lines 83 and 85). Vampire finds proofs of length 4 and 28.
\(\top\) \(\blacktriangleleft\) O
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
Such simple problems show no difference, but on hard problems Prover9 and Vampire have different strengths and weaknesses.

2.3 Throwing to satallax+

When satallax+ receives a Thm of the higher-order language, it converts it into THF format and throws it to Satallax.
\(\top\) \(\blacktriangleleft\) O
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
Satallax always does higher-order proof search, so for first-order content it often takes longer than Prover9 and Vampire.

2.4 Throwing to hyperion as well

For a long proof, the prf is written in steps. In source line 100 we have written out even the intermediate transformations. It uses the notation Le1 <- … -| ….
hyperion does no proof search; it joins Thms that have become OK so far by fixed rules (composition, removing slash, ∀-introduction, etc.) and assembles them into the form of the Thm.
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則

2.5 An example that easily trips you up

The following Thm passes the review properly.
\({\perp}\) \(\blacktriangleleft\) \(x \neq y\)
This is a property of first-order logic ( \(x \neq x\) follows from the sos).
The review is done "exactly as written". Even if you mean "two distinct x, y", it does not become so (free variables are read closed universally, so the sos is "for all x, y, x ≠ y").
In the review of the prf above on source line 105, the reviewer throws \({\perp}\) ◁ \(\neg ( x = y )\) to prover+, which throws text to Prover9, and a proof of length:2 is found.
When you want to talk about some two distinct things, write \(\mathrm{a} \neq \mathrm{b}\) with constants (\({\perp}\) ◀ \(\mathrm{a} \neq \mathrm{b}\) does not pass).
If you have doubts about the reviewer, that is the right attitude. Its soundness is given the highest importance.

2.6 Higher-order logic solvable by first-order logic

v^-Forms etc. are higher-order variables. For a Thm \(\mathcal{T}\) containing them, let \(\mathcal{T}\)|v-elim be the Thm made constant by replacing \(P\) with \(\mathrm{P}\), etc.
When there are higher-order variables, prover+ and vampire+ first apply |v-elim, and so partly decide \(\mathbb{L}_{\rm H}\) and \(\mathbb{L}_{\rm Hsc}\) too.
\({\perp} \Rightarrow P\) \(\blacktriangleleft\) O
Applying |v-elim gives \({\perp} \Rightarrow \mathrm{P}\) ◀ O.
Note that what is shown this way does not mean that a concrete formula may be substituted for \(P\) (\(P\) is a single proposition not depending on \(x\) etc.).