1 Thmelの基本

1.1 prop, Thm

p-Formの間の推論関係を扱うソフトが Thmel です。
ヘッダで .thmel ファイルを指定すると使用できます。このBookでは thmel /common/min とあり min.thmel が読み込まれます。
なおヘッダの import /common/word_logic は、論理のword（\(\top\) など）を読み込みます。だからこの Book ではそれらを紹介せずに使えます。

Thmel の定数として Formel のp-Formを登録したものをpropと言います。
prop \({\tt P}\) とpropの列 \(\Gamma\) に対し \({\tt P}\) ◀ \(\Gamma\) の形のものをThmと言います。\({\tt P}\)をgoal、\(\Gamma\)をsosと言うことがあります。
例えば　\(\top\) ◀ O　はThmです。O は空の列です。prop の代わりに式を `⊤` のように直接書くこともできます（名前の無い prop）。
列が2つ以上のときはソースで , で区切ります（表示では「，」）。
Thm を査読器が読むときは、各 prop を Formel で FCL に変換します（これを Thm の eval と言います）。

Bookにpropを載せるには、ソースに prop で始まる行を書きます。DB に登録されてあるものを使う他に、自分で <- を書いて作ることもできます。
BookにThmを載せるには、ソースに thm で始まる行を書きます。propを紹介しつつThmまで書いてしまう prop/thm もあります(ソース145行目など)。
prop \({\tt P}\) が指すp-FormをForm内で使用したいときは @\({\tt P}\) とします。乱用しない方が良いです。

1.2 Thmの変換

ThmをThmに変換することがMatheliaでは重要です。
backendごとに扱える論理が違う（次の節）ので、Thmをそのbackendが扱える言語のThmに変換してから投げるためです。

最も簡単な例として、所属言語の変換を挙げます。
Formは高階{s,c}ソート言語です。それとは別に「高階言語」があるとみなし、Thmの変換 |0 を作ります。
　\(\mathcal{T}\)が部分Formとしてc-Formを含んでいなければ \(\mathcal{T}\)|0 = (\(\mathcal{T}\)を高階言語に自然に翻訳したもの)、そうでなければ \(\mathcal{T}\)|0 はエラー
高階言語のThmは ◀ ではなく ◁ を使って作ります（説明でしか使わない記号）。また、違う言語であることを明示したいときなどにFormを緑にします。
例　(\(\top\) ◀ O)|0 \(=\) \(\top\) ◁ O
Thm \(\mathcal{T}\)に対して、\(\mathcal{T}\)|0 の eval は、\(\mathcal{T}\)を eval してから |0 を計算したものです。

1.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}\) を確かめられたときに 〇 を返す」事です。各backendが判定する論理は
　prover+ … \(\mathbb{L}_1\)
　vampire+ … \(\mathbb{L}_\mathrm{1sc}\)
　satallax+ … \(\mathbb{L}_\mathrm{Hsc}\)

1.4 定理とそのprf

一般に Thmel は \(\mathbb{L}_*\) という論理を規定します。\(\mathcal{T}\) holds in \(\mathbb{L}_*\) という形のものを「定理」と呼ぶべきです。
min.thmel では、次のように規定されています。
　\(\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}\)

BookではThmの後にはprfが書かれます（表示はされないのでprfの議論になったときはソースファイルを見て下さい）。
\(\mathcal{T}\)というThmの後のprfは \(\mathcal{T}\) holds in \(\mathbb{L}_*\) の証明とみなせるものです。
prfはThm査読において査読器に見てもらうものです。 backendの略記法が使用されます：p=prover+ v=vampire+ s=satallax+ h=hyperion
prfには例えば P ◀ Γ v; という記述がされます。査読器はそれを見ると \({\tt P}\) ◀ \(\Gamma\) を eval し vampire+ に投げます。

min.thmelには次の略記法も指定されています。
　\({\tt P}\) -| \(\Gamma\) … (\({\tt P}\) ◀ \(\Gamma\))|0
prfには P -| Γ p; という記述もよくされます。査読器はそれを見ると \({\tt P}\) -| \(\Gamma\) を eval し prover+ に投げます。

「どういうときにどのbackendに投げるべきか」は、AI用tutorialに実測の例がまとめてあります。