← ファイル一覧
（保存にはログインが要ります）
0_tutorial/3_Thmel.book
ヘッダ
行番号
title Thmel author admin mathel default thmel default
txt p-Formたちの推論関係の記述をするための言語が<b>Thmel</b>です。 txt Thmelを使用するためにはヘッダで .thmel ファイルを指定する必要があります。 txt このbookでは「thmel default」と記述されており、default.thmel が読み込まれます。 br txt .thmelファイルにはThmelのオプションが色々記述されます。 txt 一階論理は常に使用できますが、オプション設定で高階論理も使用できます。 br txt 最も簡単な例を挙げましょう。 word ⊤ thm `⊤` -| O prf `⊤` p-| O ; txt この形のものをThmと言います。左辺をgoal、右辺をsosと言います。 br txt Matheliaの使い方の基本は「数学を書く → 機械に見てもらう」です。 txt 下にある「Thm査読」ボタンを押してみてください。「OK」をクリックすると、Prover9が「length:2 の証明を見つけた」と言ったのが分かるはずです。 txt 「Thm査読」ではprfがチェックされます。表示はされませんが「`⊤` p-| O ;」と書かれています。 txt p-| はprover+に投げられることを意味します。prover+は受け取ったThmをProver9というソフトに、証明しやすい形にしてから投げます。 txt なお、各bookは独立していなければなりません。査読はそのbookに書かれていることのみを使って行われます。 br txt 「Thm査読」は、bookに書かれたThmを上から順に機械に確かめさせる仕組みです。 txt prfの各段は、その綴りが指す投げ先へ送られます。OKは「Prover9が証明を見つけた」という意味です。 txt 仮定になるのは -| の右に書いたものだけで、機械が公理を足すことはありません。 txt prfの最後の段がthmの主張になっていなければ、そこで落ちます。 br txt 査読はそのbookが「その位置までに紹介したもの」だけで行われます。 txt まだ紹介していないwordやPropを使うと落ちます。つまりbookは上から読めば辿れる一本道になります。 txt なお査読されるのは保存済みの .book で、結果は保存されません（その場の判定です）。
保存にはログイン（ページ編集の権限）が要ります。