p-Formたちの推論関係の記述をするための言語がThmelです。
Thmelを使用するためにはヘッダで .thmel ファイルを指定する必要があります。
このbookでは「thmel default」と記述されており、default.thmel が読み込まれます。

.thmelファイルにはThmelのオプションが色々記述されます。
一階論理は常に使用できますが、オプション設定で高階論理も使用できます。

最も簡単な例を挙げましょう。
\(\mathbb{W}\)(,p) … \(\top\)
\(\top\) \(\blacktriangleleft\) O
この形のものをThmと言います。左辺をgoal、右辺をsosと言います。

Matheliaの使い方の基本は「数学を書く → 機械に見てもらう」です。
下にある「Thm査読」ボタンを押してみてください。「OK」をクリックすると、Prover9が「length:2 の証明を見つけた」と言ったのが分かるはずです。
「Thm査読」ではprfがチェックされます。表示はされませんが「\(\top\) p-| O ;」と書かれています。
p-| はprover+に投げられることを意味します。prover+は受け取ったThmをProver9というソフトに、証明しやすい形にしてから投げます。
なお、各bookは独立していなければなりません。査読はそのbookに書かれていることのみを使って行われます。

「Thm査読」は、bookに書かれたThmを上から順に機械に確かめさせる仕組みです。
prfの各段は、その綴りが指す投げ先へ送られます。OKは「Prover9が証明を見つけた」という意味です。
仮定になるのは -| の右に書いたものだけで、機械が公理を足すことはありません。
prfの最後の段がthmの主張になっていなければ、そこで落ちます。

査読はそのbookが「その位置までに紹介したもの」だけで行われます。
まだ紹介していないwordやPropを使うと落ちます。つまりbookは上から読めば辿れる一本道になります。
なお査読されるのは保存済みの .book で、結果は保存されません（その場の判定です）。