1 例から

1.1 最初のThm

この Book は Thmel（定理とその証明の書き方）の説明です。ヘッダに thmel 行が無いので default.thmel を読み込んでいます。
まず、いちばん小さい定理を書きます。ソースは次の2行です。
　thm `⊤` ◀ O
　prf `⊤` -| O p;
\(\top\) \(\blacktriangleleft\) O
1行目（thm）が主張です。「O（前提なし）から ⊤ が推論できる」と読みます。◀ の左を goal、右（前提の列）を sos と言います。O は空の列です。
2行目（prf）が証明の指示で、表示はされません（ソースで読みます）。「(⊤ ◀ O) を -| の変換にかけて p（prover+。内部で Prover9 を使う）に投げる」と読みます。末尾の1文字が投げ先（どの backend に投げるか）です。
thm は ◀、prf の段は -| ですが、それで構いません。段 goal -| sos が OK なら、thm goal ◀ sos は示されたことになります（Thmel が -| を「◀ の Thm を変換して確かめる」ものと規定しているため・「仕組み」の節）。1.book の例のように ◀ のまま ◀ … p; と書いても OK で、違うのは投げ方と速さです（次の節）。
右の「査読（この頁）」ボタンを押すと、Thm査読の表に「OK」と出ます。#列の 1.1-1 は 1.1節の1番目の Thm です。OK をクリックすると 〇 の印が出て、Prover9 が length:2 の証明を見つけたことが分かります（〇＝backend が確かめた印）。投げた入力はコレです（\(\top\) は $T）。
〇 の印を押すと開く小窓（投げた入力）では、証明器に渡すために処理した問題と、証明器への入力の原文を照合できます。上から次の順に並びます。
　① # prover+ が受け取ったもの … 翻訳した後・分割する前の前提（assumptions）と goal。この例（-| … p;）では JSON で書いた前置記法（2.book）で、goal が "⊤"、前提はありません。多ソートの段（◀ や --| の段）では、ソート付きの木の JSON で出ます
　② # prover+ がProver9に投げた … goal を分割したときは「2つにsplitして」のように本数が付きます。prover+ は、分割したすべてが proved のときに元の段を認めます。strategy は前処理の方式の名前です
　③ 1本ごとに、# 1/2 prover+ が割った1本（分割する前と同じなら出ません）と、# 1/2 Prover9 に投げた の下に Prover9 への入力の原文
小窓に出ないものもあります：slash や翻訳の途中の書き換え、証明器が返した証明。ですから、小窓だけで書いた段から 〇 までを確かめられるわけではありません。例えば articles1/63.book の証明①の主定理 X <# ℘ X の1段目では、/ <#. で goal が「≤# かつ ¬=#」に開いたものを prover+ が受け取り、2本に分割して Prover9 に投げたことまでが読めます。

1.2 前提のあるThm

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
ソース：
　word + … 記号 + を紹介する（gram (ss,s)。+ の意味は決めていない＝前提が唯一の手がかり）
　prop +結合則 <- `x + (y + z) = (x + y) + z` … 式に名前を付ける（prop）。x, y, z は自由変数で、「すべての x, y, z について」の意味
　thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 … 主張を式で書いた thm。その prf の中では goal がこの式を指す
　prf goal -| +結合則 p; … 前の例と同じ指示を、名前で書いたもの
投げた入力はコレで、length:5 の証明が見つかります。Prover9 への入力に + の gram は書かれません。

1.3 同じThmを別の投げ先へ

同じ Thm に、投げ方だけ違う prf を付けます。どれも OK です。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal ◀ +結合則 v; … -| の変換をせず（◀ のまま）v（vampire+。内部で Vampire を使う）へ。ソート s を型として保ったTFF形式で投げます（plus: (mathel_s * mathel_s) > mathel_s が + の型）。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal -| +結合則 s; … -| の変換をして s（satallax+。内部で Satallax を使う）へ。THF形式で投げます（関数はカリー化 plus @ X @ Y）。
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
　prf goal ◀ +結合則 p; … -| の変換をせず p へ。prover+ が自分でソートを一項述語にして（相対化・6節）コレを投げます。約400ms・length:18 で、-| p; より遅くなります。

2 書き方の一覧

2.1 prf の1段

prf の1段は goal 関係 sos 投げ先; です（例 goal -| +結合則 p;）。sos が複数なら ,（前後に半角スペース）で区切ります。関係と投げ先の組み合わせ：

書き方	投げる前にすること	c-Form を含むThm
goal -| sos p;　goal -| sos v;　goal -| sos s;	Thm 全体を |0 で「高階言語」へ変換（「仕組み」の節）	-| は Thm を |cvt+|0（5.book）で翻訳する＝クラスの語は定義で開く。クラス変数（X_ など）が残ると |0 がエラーで FAIL。クラス変数は ◀ … v; か --| … v; で扱う
goal ◀ sos p;	-| の変換はしない。prover+ がソートを一項述語にして相対化し、一階言語へ	扱える
goal ◀ sos v;	-| の変換はしない。vampire+ がソートを型として保った TFF にする	扱える
goal ◀ sos h;	証明器に投げない。前の段で示した Thm を組み合わせて主張を導く	—

goal ◀ sos s; も書けます（この Book では扱いません）。

--|（{s,c}ソートのまま翻訳）も書けます（5.book）。

2.2 backend

段の末尾の文字（p v s h）を投げ先、それが指すソフト（prover+ など）を backend、backend が中で使う Prover9・Vampire・Satallax を証明器と言います（h の hyperion は下の h の行）。
　p … prover+：Prover9 を使う。一階論理 \(\mathbb{L}_1\) を判定。◀ で受けたときは一階翻訳をして \(\mathbb{L}_\mathrm{1sc}\) も判定（6節）
　v … vampire+：Vampire を使う。一階{s,c}ソート論理 \(\mathbb{L}_\mathrm{1sc}\) を判定
　s … satallax+：Satallax を使う。高階{s,c}ソート論理 \(\mathbb{L}_\mathrm{Hsc}\) を判定
　h … hyperion：証明器ではなくメタ推論のソフト。式の証明探索はせず、示した Thm を組み合わせるだけなので、証明器を待つ時間がかからない（例外は、関係をまたいで Thm を確かめ直すときに Vampire を呼ぶこと。W. を含む Thm の確かめ直しは何分もかかることがある・下の「h; の段の関係」）
1節の例（◀ … p; を除く）の時間は、Prover9・Vampire は約10ms（ほぼプロセス起動の分）、Satallax は \(\top\) で10ms・結合則で600ms程です。Satallax は常に高階の探索をするので、一階の内容には割に合わないコストがかかります。

3 仕組み

3.1 prop と Thm

Thmel の定数として Formel の p-Form を登録したものをpropと言います。prop は DB に登録されたものを使うほか、prop名 <- `…` で作れます。
prop \({\tt P}\) と prop の列 \(\Gamma\) に対し \({\tt P}\) ◀ \(\Gamma\) の形のものをThmと言います。Thm の eval は各 prop を Formel に投げ FCL に変換したものです。
prop \({\tt P}\) が指す p-Form を式の中で使うときは @\({\tt P}\) と書きます。使えるのはThmの中と、Book で作る prop の本文です。ふつうは prop を sos に名前で置けば足ります。

3.2 Thmの変換 |0

backend ごとに扱える論理が違うので、Thm をその backend が扱える言語の Thm に変換してから投げます。変換を |f と書き、\(\mathcal{T}\)|f の eval は \(\mathcal{T}\) を eval してから |f を計算したものです。
Form は高階{s,c}ソート言語です。それとは別に「高階言語」（ソートの無い言語）があるとみなし、変換 |0 を作ります。
　\(\mathcal{T}\) が部分Formとして c-Form を含まなければ \(\mathcal{T}\)|0 = (\(\mathcal{T}\) を高階言語に自然に翻訳したもの)、含めば \(\mathcal{T}\)|0 はエラー
高階言語の Thm は ◀ ではなく ◁ で書きます（説明でしか使わない記号）。違う言語であることを示すため、式を緑にします。例　(\(\top\) ◀ O)|0 \(=\) \(\top\) ◁ O
Thmel は goal -| sos を (goal ◀ sos)|cvt+|0 と規定しています（|cvt+ は 5.book。c-Form を含まない Thm では何もしない）。|0 がエラーになる段は査読の失敗です。

3.3 論理と定理

Thm は形式的なものです。Thm に意味を与えるものを論理と言います。Thm \(\mathcal{T}\) を論理 \(\mathbb{L}\) で扱え、◀ を「推論できる」と読めるとき、\(\mathcal{T}\) holds in \(\mathbb{L}\) と書きます。
Mathelia では 高階{s,c}ソート論理 \(\mathbb{L}_{\rm Hsc}\) と 高階論理 \(\mathbb{L}_{\rm H}\) は既知とし、通常はその部分論理 一階{s,c}ソート論理 \(\mathbb{L}_{\rm 1sc}\) と 一階論理 \(\mathbb{L}_1\) を使います。\(\mathbb{L}_1\) の公理には等号公理と領域の非空性 \(\exists x \, ( x = x )\) が含まれます。
backend が「\(\mathbb{L}\) を判定する」とは「Thm \(\mathcal{T}\) を受け取ったとき、\(\mathcal{T}\) holds in \(\mathbb{L}\) を確かめると 〇 を返す」ことです。
Thmel は論理 \(\mathbb{L}_*\) を規定し、\(\mathcal{T}\) holds in \(\mathbb{L}_*\) の形のものを「定理」と呼びます。c-Form を含まない Thm についての規定（c-Form を含む場合は 5.book）：
　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\) holds in \(\mathbb{L}_\mathrm{Hsc}\)
　\(\mathcal{T}\)|0 がエラーでなければ　\(\mathcal{T}\) holds in \(\mathbb{L}_*\) \(\Longleftrightarrow\) \(\mathcal{T}\)|0 holds in \(\mathbb{L}_\mathrm{H}\)
Thm の後の prf は \(\mathcal{T}\) holds in \(\mathbb{L}_*\) の証明とみなせるもので、Thm 査読で査読器に見てもらいます。