book集

section 例で見るMathelia
txt Matheliaは堅牢な数学を作成するためのソフトです。数学はBookに書き、それを機械が検査（査読）します。
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px">Matheliaは、AI が Book を書き、人間はできた Book を鑑賞するという使い方を想定しています。そのため書き方には曖昧さを残さず、書いたものは書いた通りに、すべて機械的に検査されます。この Book は、AI（と人間）が最初に読む説明です。</div>
txt 3つの例で、①Thm と prf、②記号の紹介と前提、③定数と前提の足りないとき、を順に見ます。どの例もこのBookに実際に書かれていて、査読を通ります。
txt 以下では、ソースの行を説明のために <code>このような表示</code> で再掲します。.bookファイルにはその行をそのまま書きます。式はバッククォート &#96; &#96; で囲んで書きます。

subsection 例1　Thm と prf
thm `x = y ⟹ y = x` ◀ O
prf `x = y ⟹ y = x` ◀ O p;
txt ソース（.bookファイル）では次の2行です。
txt <code>thm &#96;x = y ⟹ y = x&#96; ◀ O</code>
txt 　thm はThm（主張）を書く命令です。A ◀ Γ は「◀ の右に並べた前提の列 Γ から、左の式 A が推論できる」と読みます。A を goal、Γ を sos（set of support＝前提の集まり）と言います。
txt 　O（大文字のオー）は空の列です。この例では ◀ の右に前提が何も無く、x = y は主張する式 x = y ⟹ y = x の一部です。
txt 　x, y は変数で、「すべての x, y について」の意味になります。
txt 　= と ⟹ は、ヘッダの <code>import /common/word_logic</code> で読み込んだ Book が紹介済みの記号なので、そのまま使えます。その Book が紹介している主な記号は次のとおりです。
txt 　　⊤（真）　⊥（偽）　¬（否定）　and（かつ。表示は「,」）　or（または）　⇒ ⇔（ならば・同値）　⟹ ⟺（結合の弱い ならば・同値）　∀ ∃　=　{/}（否定。x {/}= y は x ≠ y）
txt 　結合は、+ などの演算が = より強く、= が and より強く、and が ⟹ より強くなります（x = y and y = z ⟹ x = z は (x = y and y = z) ⟹ x = z）。迷ったら括弧を付けます。
txt <code>prf &#96;x = y ⟹ y = x&#96; ◀ O p;</code>
txt 　prf は直前の Thm の確かめ方を書く所で、表示はされません。確かめ方はいくつかの段階に分けて書くこともできますが、この例は1回で済むので、Thm と同じ形をそのまま書き、末尾に投げ先を付けます。
txt 　p; は「prover+（内部で自動定理証明器 Prover9 を使う）に投げる」という意味です。自分で証明を1歩ずつ書く代わりに、証明器に「この前提からこの式が出るか」を探させます。投げ先はほかに v; s; h; があります（3.book）。
txt ここまでで最小のBookが書けます。次の7行が Mathelia の「Hello World」です。まずこれを動かしてください。Bookの一覧のページ（/book_collection/）で新しいBookを作り（ログインが必要）、7行を写して保存し、査読すると OK になります。
txt 　文字コードは UTF-8（BOM なし）です。⟹ ◀ などの記号は Unicode の文字そのもので書くので、この頁からコピーするのが確実です。ログインせずに作業するときは、同じ内容を .bookファイルとして置いて CLI で査読します（「CLIから査読する」の章）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">title 最初のBook import /common/word_logic formel /common/default thmel /common/min --- thm &#96;x = y ⟹ y = x&#96; ◀ O prf &#96;x = y ⟹ y = x&#96; ◀ O p;</div>

subsection 例2　記号の紹介と前提
word +
prop +結合則 <- `x + (y + z) = (x + y) + z`
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 p;
txt 「結合則を満たす演算なら、4つの項でも括弧を付け替えられる」という定理です。ソースでは次の4行です。
txt <code>word +</code>
txt 　記号 + は import した Book が紹介していないので、使う前に紹介します。表示の (ss,s) は + のgramで、「s-Form（項）を2つ受け取り s-Form を返す」＝2項演算であることを表します。gram は DB に登録されていて、紹介すると表示されます。
txt 　ここでは + の意味（数の足し算など）は何も決めていません。分かっているのは次の前提だけです。
txt <code>prop +結合則 &lt;- &#96;x + (y + z) = (x + y) + z&#96;</code>
txt 　prop は式に名前を付けます。名前を付けただけで、証明されたわけではありません。ここでは前提として ◀ の右に置きます。x, y, z は量化子（∀ ∃）で縛られていない変数なので、前提としても「すべての x, y, z について」の結合則になります。
txt <code>thm &#96;x + (y + (z + w)) = ((x + y) + z) + w&#96; ◀ +結合則</code>
txt <code>prf &#96;x + (y + (z + w)) = ((x + y) + z) + w&#96; ◀ +結合則 p;</code>
txt 　結合則を仮定しない演算では、この等式は一般には成り立ちません。実際、thm と prf の両方で ◀ の右の +結合則 を O に替えると、証明は見つからず、査読は FAIL になります。FAIL は「この前提からは確かめられなかった」ということで、主張が偽だという判定ではありません。

subsection 例3　定数と、前提の足りないとき
word ∈
prop 仮定1 <- `∀ x (x ∈ |A ⟹ x ∈ |B)`
prop 仮定2 <- `|a ∈ |A`
thm `|a ∈ |B` ◀ 仮定1 ,, 仮定2
prf `|a ∈ |B` ◀ 仮定1 ,, 仮定2 p;
txt 「A のどの元も B に属し、a が A に属するなら、a は B に属する」という定理です。ソースでは次の5行です。
txt <code>word ∈</code>
txt 　表示の (ss,p) は、∈ が「s-Form を2つ受け取り p-Form（命題）を返す」ことを表します。例2の + は項を返し、∈ は命題を返します。
txt <code>prop 仮定1 &lt;- &#96;∀ x (x ∈ |A ⟹ x ∈ |B)&#96;</code>
txt <code>prop 仮定2 &lt;- &#96;|a ∈ |A&#96;</code>
txt 　|A, |B, |a のように | を付けたものは定数です。紹介せずに使えます。表示では | は消え、定数は立体（a）、変数は斜体（x）で示されます。
txt 　例2で見たとおり、量化子で縛られていない変数は、前提の中でも「すべての値について」の意味になります。仮定1 の ∀ x は省いても同じ意味ですが、読みやすさのために書いています。
txt 　一方、仮定2 を |a ∈ |A でなく a ∈ A と書くと「すべての a, A について a ∈ A」という強すぎる前提になり、意図した定理ではなくなります。特定のものについて述べるときは定数を使います。
txt <code>thm &#96;|a ∈ |B&#96; ◀ 仮定1 ,, 仮定2</code>
txt 　前提が2つ以上あるときは ,, で区切ります（表示では「，」になります）。
txt <code>prf &#96;|a ∈ |B&#96; ◀ 仮定1 ,, 仮定2 p;</code>
txt 　thm と prf の両方で ◀ の右を 仮定1 だけにする（仮定2 を外す）と、証明は見つからず、査読は FAIL になります。

section Bookの書き方
txt Bookは .bookファイル に記録され、表示ソフトで閲覧されます。
txt .bookファイルはヘッダと本文からなり、両者は --- という行で区切られます。各行は原則として<note>命令語で始まります<?>この行は txt という命令語で始まっています。命令語の一覧は後半の「辞書」の章にあります</note>（例外は、字下げして次の行に続けた prf の続きです）。上の例では thm・prf・word・prop が本文の命令語です。
txt ヘッダの行は次の意味です。
txt 　<code>title</code> … Bookの題。<code>author</code> … 書いた人。
txt 　<code>import /common/word_logic</code> … = ⟹ ∀ などの論理の記号を紹介済みの Book を読み込みます。書くときは .book を付けません（表示では付きます）。
txt 　<code>formel /common/default</code>、<code>thmel /common/min</code> … 式の言語と、Thm・証明の扱いを決める設定ファイルを指定します。
txt 保存すると、まずコンパイルで「書法にエラーが無く表示ができるか？」「他ファイルの読み込みはちゃんとできるか？」がチェックされ、表示されます。証明が正しいかは、次の査読で確かめます。

section Bookの査読
txt 査読はMatheliaの最も重要な機能で、「まだ紹介されてない記号が無いか？」「証明が正しいか」などを、文字通り「機械的に」チェックします。
txt それは、上から順に、そのBook（とimportされたBook）の「その位置までに紹介されたもの」に書かれていることだけで行われます。なおtxt行は人間のための説明であり査読では無視されます。
txt Bookを表示すると、各頁に「査読（この頁）」というボタンが出ます。押すと、紹介査読（語・Prop などが使う前に紹介されているか）と Thm査読の結果が続けて出ます（両方 OK なら「査読: ALL OK」）。ヘッダに option review quick:true; と書いた本には「簡易Thm査読（この頁）」も出ます。結論のつなぎ（Hyperion）などを省いた速さ優先の Thm査読で、prf を試すときに使います（その OK は〇の根拠にはなりません）。Thm査読の表には Thm ごとに番号（#1.2-1 は 1.2 節の1番目の Thm。subsection の前にある Thm は #1-1 のように節番号だけ）と結果（通れば処理時間を添えた OK＝例 0.12秒 OK、落ちれば FAIL と理由）が並んで表示されます。
txt FAIL は査読に通らなかったことを示します。理由には、証明が見つからない場合（例2・例3の前提を外したとき）のほか、未紹介の記号を使った場合などがあります。例えば例2で word + の行を消すと、「本が紹介していない word を Form の中で使っています: +」という理由で FAIL になります。
txt 　CLI での査読結果は、例えば次のような行で返ります（Thm の番号・Thm または ファイル:行・結果）。
txt 　<code>#1.1-1　\(x = y \Longrightarrow y = x\) ◀ O　0.12秒 OK</code> 　<code>#1.2-1　1.book:30　FAIL: 本が紹介していない word を Form の中で使っています: +</code>
txt 　DB に無い記号を word で紹介しようとすると、査読より前のコンパイルの時点で「word は言語に無い綴りです: ♠」のようなエラーになり、表示もできません。
txt FAIL のときは理由を読み、記号を紹介する・前提を足す・証明を段に分ける（3.book）などをしてから、保存し直して再び査読します。
txt 査読されるのは保存済みの .book です。結果は頁ごとに保存され、前の頁やimportした本は、中身が変わっていなければ査読し直さず、保存された結果を使います。

section CLIから査読する
txt ブラウザの査読ボタンを押せない場合（AIエージェントが対話画面を持たずに作業しているときなど）は、Web画面の「査読」ボタンと全く同じ査読（紹介査読と Thm査読）をCLIから実行できます。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/review_cli.php &lt;本の名前&gt; [頁番号] [--inputs]</div>
txt &lt;本の名前&gt;はフォルダ名/本の名前（拡張子なし。例 standard_math/1）。頁番号は1から数え、省略すると本全体を査読します（「option review per-page:false;」を宣言した本では頁番号は効きません）。Webのエディタでも編集できるように、置いたファイルはグループを www-data、パーミッションを 664 にしておきます。
txt 実行すると、紹介査読の件数（落ちた行があれば行番号と理由）、各Thmの番号・結果（OK／FAIL、FAILなら理由）、全体の判定（例 総合判定: ALL OK（紹介査読 OK／Thm査読 OK））をプレーンテキストで返します。終了コードは0＝ALL OK、1＝紹介査読か Thm査読に FAIL あり、2＝引数や本の指定の誤り、3＝判定できない（コンパイルエラーなど。総合判定は「不明」）です。<code>--inputs</code> を付けると、FAIL した行の下に、落ちた段が証明器へ投げた入力（翻訳した後の式）を出します。どの定義が開かずに残ったかなど、FAIL の原因を読むのに使います（6b.book）。式の読まれ方や slash の書き換えだけを確かめるときは、証明器に投げない次のコマンドを使います（2.book・4.book）。
txt <div style="font-family:monospace;background:#f4f4f4;border:1px solid #ddd;padding:6px 10px;overflow-x:auto;white-space:nowrap">cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/slash_cli.php &lt;本の名前&gt; '&#96;式&#96; // W.'</div>
txt 式だけを書くと読まれ方（前置記法）が、<code>// W.</code> などを付けると書き換えた結果が返ります。自分で書いたThmが正しいかを確かめるのは、上の review_cli です。

section 次にすること
txt 〇例1の7行のBookに、例2・例3を書き足してみてください。
txt 〇ログインせずに作業するとき（AIエージェントなど）は、.bookファイルを /var/www/test2.atp-research.com/wp-content/themes/lightning/mathelia/フォルダ/名前.book に置き、上の「CLIから査読する」のコマンドで査読します。
txt 〇続きは 2.book（式の書き方 Formel）、3.book（Thmと証明 Thmel）、4.book（高度な表現）、5.book（ものとクラス）、6.book（集合とクラス）、6b.book（実践：投げ先・失敗・戦略）へ。
br
txt ★Matheliaの仕様はまだ未確定のものも多いです。使用された方からの「こういう機能が欲しい」という建設的な意見をお待ちしております。

section Matheliaの部品
txt Matheliaは内部で独立性の高い部品を多く持っています。
txt 〇DB (データベース)は word・prop などのデータを保存します。
txt 〇数学の記述においては、Form（項や命題を表す記号の列）を扱う Formel、Thm を扱う Thmel が使用されます（詳しくは2.book, 3.book）。
txt 〇Thmを査読する backend(prover+, vampire+, satallax+, hyperion) はMatheliaの心臓部と言えます。prover+ は <a href="https://prover9.org/">Prover9</a> を、vampire+ は <a href="https://vprover.github.io/">Vampire</a> を、satallax+は <a href="https://www.ps.uni-saarland.de/~cebrown/satallax/">Satallax</a> を内部に持ちます。
txt 〇Mathelia本体はファイル操作・Book操作などを行う他、各部品間の橋渡しをします。
txt Bookの堅牢さを保証するためには、各部品を堅牢にし、部品間の情報のやり取りの流れを明瞭にすることが大事です。

section ファイルの基本
txt .bookファイルは文字コード UTF-8（BOM なし）で書きます。改行は LF でも CRLF でも構いません。
txt 　Shift_JIS などで保存すると「UTF-8 ではない文字があります」、BOM 付きの UTF-8 で保存すると「先頭に BOM があります」というコンパイルエラーになります。⟹ ◀ などの記号は Shift_JIS では表せません。
txt 記号は Unicode の文字そのもの（⟹ ∀ ∈ ◀ など）で書きます。これらの記号の以前の ASCII の綴り（==> all in など）は使えません。
txt 変数は英字1文字に数字や ' を付けたもの（x, A, x1, x'）とギリシャ文字（α, α1）などです。定数はその前に | を付けたもの（|a, |A1）です。
txt フォルダ名・Book名には半角の英数字と _ - を使います（例 0_tutorial_AI/1）。
txt 1行に1つの命令を書きます。長い prf だけは、次の行を字下げして続けられます。
txt 見た目が似ていても別の文字です。取り違えたときに出るエラーも挙げます。
txt 　⟹ と ⇒ … どちらも Formel の記号で、結合の強さが違います（2.book）。取り違えてもエラーにならないので注意します。
txt 　半角スペースと全角スペース … 命令語の後が全角だと「Unknown line kind」、式の中だと「この Formel の語でも変数・定数の綴りでもありません」。
txt 　&#96;（バッククォート）と &#8216; … thm で &#8216; を使うと「&#8216;式&#8216;（一階言語の式）は txt 行だけで使えます」。
txt 　∈ と ε … ε はギリシャ文字の変数になり、「Formとして消費されないwordがあります」。
txt 　◀ と ◁ … prf で ◁ を使うと「prf の段に書けない演算子です: ◁」。
txt 　-| の - と − （マイナス記号 U+2212）… thm で − を使うと「「−」（U+2212 マイナス記号）が使われています」。
txt 　,, と ，・、 … 前提の区切りに ， や 、 を使うと「前提（sos）の区切りは半角の ,, です」。
txt 　O（大文字のオー）と 0（ゼロ）… ◀ 0 は「unintroduced sos name: 0」。
txt 　∅ と Ø … Ø は「この Formel の語でも変数・定数の綴りでもありません」。

newpage

section 辞書：命令語とオプションの一覧
txt <div style="border-left:4px solid #0b64c8;background:#f3f7ff;padding:6px 10px">ここから先は辞書です。初めて読むときは飛ばして 2.book へ進んで構いません。コンパイルエラーや査読エラーが出たとき、書き方を確かめたいときに引いてください。</div>
txt Bookのソース（.bookファイル）を書くための命令語・ヘッダ・オプションの一覧です。使い方の説明と例は 0_tutorial_AI の 2〜5.book にあります。
txt Bookは mathelia/フォルダ/名前.book に置きます。本の名前は「フォルダ/名前」（拡張子なし。例 standard_math/1）で指します。
txt 各行は「命令語 引数」の形です。命令語と引数の間は半角スペースです（全角スペースは区切りになりません）。空行は無視されます。
txt 命令語の頭に ! を付けたもの（!prop !thm など）は、表示しないが査読には使う版です。ただし <code>!txt</code> だけは表示も査読もされないメモです。
txt 知らない命令語や書き方の誤りは、コンパイル時に「ファイル:行番号 理由」の形のエラーになります。
txt 以下で <code>&#96;式&#96;</code> はバッククォートで囲んだ Formel の式、<code>名</code> は空白を含まない名前です。
txt 命令語は Bookエディタと同じ色で示します：ヘッダの欄、見出し、命令、txt・br、prf と ; と投げ先、!txt、&#96;Formel の式&#96;。

subsection ヘッダ
txt ヘッダは本文の前に書き、<code>---</code> だけの行で本文と区切ります。各欄は1回だけ書けます（option を除く）。
txt <code>title 題</code> … 必須。Bookの題です。
txt <code>author 名前</code> … 任意。
txt <code>import 本 本 …</code> … 他のBookが紹介した word・prop・abbr・lower と、証明済みの Thm を引き継ぎます。import した本の証明はやり直さず、保存された査読結果を使います。<code>/</code> で始めると mathelia/ からの位置（例 <code>/common/word_logic</code>）、始めなければ同じフォルダの本です。
txt <code>formel 名前</code> … 読み込む .formel（例 <code>/common/default</code>）。本文に Formel の式を書くなら必要です。
txt <code>thmel 名前</code> … 読み込む .thmel（例 <code>/common/min</code>、<code>/common/default</code>）。thm・prf を書くなら必要です。
txt formel・thmel は import した本から引き継がれません。本ごとに自分のヘッダに書きます。
txt <code>option 対象 名前:値;</code> … 表示・査読の設定です（下の「option」の節）。何行でも書けます。
txt <code>fragments 本 本 …</code> … 別ファイルの本文を順に取り込みます（現在の Book では使っていません）。

section 本文の命令語
subsection 地の文と見出し
txt <code>section 題</code>、<code>subsection 題</code> … 見出し。番号は自動で付きます（section は n、subsection は n.m）。Thm査読の番号 #n-k は「section n の k 番目の Thm」です。
txt <code>txt 文</code> … 地の文。HTML と MathJax（<code>\(…\)</code>）が使えます。査読されません。
txt 　txt の中でバッククォートで囲んだものは Formel の式として表示されます（書く本は formel の宣言が要ります）。<code>&#8216;式&#8216;</code> で囲んだものは一階言語の式として緑で表示されます（txt 行だけ）。
txt 　<code>&lt;note&gt;A&lt;?&gt;B&lt;/note&gt;</code> は A を表示し、クリックすると B を出します。
txt <code>!txt メモ</code> … 表示されないメモです（prf の中にも書けます）。
txt <code>br</code> … 空行を入れます。引数はありません。
txt <code>newpage</code> … 頁の区切りです。査読は頁ごとに行われます（option review per-page）。画面は続けて表示し、印刷ではここで改ページします。

subsection word・abbr・lower
txt <code>word 綴り 綴り …</code> … DB にある word を紹介します。1行に並べられるのは、紹介の見出し（分類と gram）が同じ語だけです。変数・定数・引数をとる記号（<code>?f</code> <code>|?p^</code> など）は紹介しません。
txt <code>word* 綴り …</code> … word と同じ紹介で、表示の仕方だけが違います（gram をそのまま出す）。
txt <code>!word 綴り …</code> … 表示しない紹介です。
txt <code>abbr 名前</code>、<code>!abbr 名前</code> … 省略表現の規則（abbr）を紹介します。
txt <code>lower 名前</code> … word+ を FCL へ下ろす規則（lower）を紹介します。word+ を式で使うには、その lower の紹介が要ります。
txt 紹介は使うより前に書きます。査読は、その位置までに紹介されたもの（import した本の分を含む）だけで行われます。

subsection prop と let
txt <code>prop 名</code> … DB にある Prop を紹介して表示します。DB に無い名前でも、最初の数字の並びを <code>\n</code> に替えた名前の schema があれば、その実体として読みます（<code>prop ary1R</code> は <code>ary\nR</code> の n=1）。
txt <code>prop 名 &lt;- &#96;式&#96;</code> … 名前を付けた Prop を自分で作ります。
txt <code>!prop 名</code> … 表示しない紹介です。
txt <code>prop 名 &lt;- schema名[P:=&#96;θ&#96;]</code> … schema の具体例に名前を付けます（下の schema）。
txt <code>let 名 &lt;- &#96;式&#96;</code> … Book の中だけの名前を式に付けます。表示されます（<code>!let</code> は表示しない）。置き直してよく、thm・prf で使ったときの中身が使われます。
txt <code>let |C_ := &#96;項&#96;</code> … Book 内の定数（| で始まる名前）。式の中に書くと項に展開され、証明器にも届きます。こちらだけは <code>:=</code> で書きます。
txt <code>form &#96;式&#96;</code> … 式を表示するだけです（査読の対象になりません）。
txt <code>schema 名(P;x,y) := &#96;ψ&#96;</code> … 命題変数・述語変数を含む schema の宣言です（HOL.book を参照）。
txt <code>prop-family 頭 sos</code> … Prop の族を紹介します（現在の Book では使っていません）。

subsection thm と prf
txt <code>thm 主張 関係 sos</code> … Thm です。主張は Prop の名前か <code>&#96;式&#96;</code>。関係は <code>◀</code> <code>-|</code> <code>--|</code> で、どれが使えるかは .thmel が決めます。sos は <code>,,</code> で区切った Prop の列、空の列は <code>O</code> です。主張が <code>&#96;式&#96;</code> のとき、prf の中では <code>goal</code> がその式を指します（prf の中で自分で <code>goal &lt;- …</code> と書くとその Thm の査読エラー）。
txt <code>prop/thm 名 関係 sos</code> … <code>prop 名</code> と thm を1行に。<code>prop/thm 名 &lt;- &#96;式&#96; 関係 sos</code> とも書けます。
txt <code>let/thm 名 &lt;- &#96;式&#96; 関係 sos</code> … let と thm を1行に。名前は後の Thm でも使えます（その Thm の prf の中だけで式を呼ぶなら <code>thm &#96;式&#96;</code> と <code>goal</code> で足ります）。
txt <code>!thm</code> <code>!prop/thm</code> <code>!let/thm</code> … 表示しない版です（査読はされます）。
txt 行の末尾に <code>at \n=2..5</code> と書くと、n=2〜5 のそれぞれを査読します。確かめるのは書いた n だけです（すべての n についての証明ではありません）。
txt <code>prf 段 ; 段 ; …</code> … 直前の thm の証明です。thm の後、次の thm の前に1つだけ書きます（間に txt などがあってもよい）。長いときは、次の行を字下げして続けます。prf は表示されません。

subsection prf の段
txt 段は <code>;</code> で区切ります。証明器に投げる段は「主張 関係 sos 投げ先;」の形です。例 <code>&#96;x = y ⟹ y = x&#96; ◀ O p;</code>（第1頁の例1）
txt 投げ先の文字は .thmel の backend が決めます（p＝prover+、v＝vampire+、s＝satallax+、h＝hyperion）。投げ先は <code>;</code> の直前に空白なしで付けます。関係（◀ -| など）を含む段に投げ先が無いと査読エラーです（下のラベルだけの段は投げ先を持ちません）。
txt <code>p[whole];</code> … goal を断片に割らずに1つの問題として投げます。
txt 投げた段が OK になると、その段の Thm が既知の Thm として積まれます。
txt <code>名 &lt;- &#96;式&#96; ;</code> … prf の中だけのラベル（補題の式）。使うより前に書きます。<code>名 &lt;- &#96;式&#96; 関係 sos p;</code> とすると、ラベルを付けてすぐ投げる1段になります。同じ prf で同じラベルを2回定義すると査読エラーです。
txt <code>主張 関係 sos h;</code> … hyperion に投げる結論の段。積まれた Thm から thm の主張を導けるかを確かめます。1つの prf に結論の段は1つだけです。
txt 投げた段がそのまま thm の主張を示しているとき（3.book の最初の例）は、結論の段は要りません。
txt 段の中の主張には、次のものが使えます（説明は 4.book。以下の 〇 は Prop の名前を入れる所です）。
txt 　<code>A / 〇.</code>（〇. で展開）　<code>//</code>（2回）　<code>/n 〇.</code>（n 番目だけ）　<code>W.</code>（定義の列）　<code>W.!〇.</code>（W. から 〇. を除く。空白を入れない）　<code>W.'</code>（証明済みの別定義を使う W.）
txt 　<code>@〇</code>（Prop 〇 が指す式・Thm の中だけ）
txt 　段の末尾（投げ先の前）の <code>{〇.'}</code>（別の定義でその段を翻訳）、<code>{〇.-}</code>（クラスへの所属を新しい述語に置き替える）
txt 　<code>主張 [&amp;l -| A || &amp;r -| B] p;</code>（主張を連言の左右で分ける。<code>[⇒ … || &lt;= …]</code> は同値の向き）

section option と .thmel・.formel
subsection option
txt ヘッダに <code>option 対象 名前:値;</code> と書きます。宣言は <code>;</code> で区切り、1行に複数書けます。同じ宣言を2度書くとエラーです。
txt <code>option section format:第%n章　%t;</code> … section の見出しの形。<code>%n</code>（番号）と <code>%t</code>（題）をちょうど1つずつ含めます。既定は <code>%n %t</code>。
txt <code>option review per-page:false;</code> … 既定は true＝各頁に「この頁」の査読ボタンが出ます。false にすると最終頁に本全体の査読ボタンが出ます。
txt <code>option review quick:true;</code> … 既定は false。true にすると「査読」の隣に「簡易Thm査読」のボタンが出ます。結論のつなぎ（Hyperion）などを省いた速さ優先の Thm査読で、Book を書く・prf を試す段階に使います。結果は保存されず、その OK は〇の根拠になりません。
txt <code>option review original-relation:true;</code> … 本全体の査読ボタンの横に「原関係照合まで」のボタンを出します（現在の Book では使っていません）。

subsection .formel の行
txt Formel の言語を決めるファイルです。今あるのは common/default.formel です。
txt <code>name letter A-Z a-z</code> … 文字の集まりに名前を付けます。
txt <code>form s c p</code> … 使う Form の型。
txt <code>word tex_only \, \; \! !, { } _ ^</code> … 表示だけに使い、FCL 変換では無視する語。
txt <code>[lDP] [letter][0-9]*'*</code> … 正規表現に名前を付けます。
txt <code>word v-Form [lDP]</code> など … 変数・定数・引数をとる記号の綴りを正規表現で決めます。
txt <code>word ∈_</code> など … この環境で紹介なしに使える word。

subsection .thmel の行
txt thm・prf の関係と投げ先を決めるファイルです。今あるのは common/min.thmel（0_tutorial_AI の 1・3・4.book）、common/default.thmel（標準）、common/zf.thmel（default に satallax+（s;）を加え、Vampire の待ち時間を長くしたもの）です。
txt 3つの .thmel の違い（ファイルの記述そのまま・2026-09-29）：
txt <table border="1"><tr><th></th><th>min</th><th>default</th><th>zf</th></tr><tr><td>投げ先（target）</td><td>p v s h</td><td>p v h</td><td>p v s h</td></tr><tr><td>ソート（sort）</td><td>s c</td><td>s c f（\fn などを送れる）</td><td>s c f</td></tr><tr><td>-| の行</td><td colspan="3">3つとも同じ <code>goal -| sos &lt;-&gt; (goal ◀ sos)|cvt+|0</code></td></tr><tr><td>--| の行</td><td>無い（書くと査読エラー）</td><td colspan="2"><code>goal --| sos &lt;-&gt; goal|sc ◀ sos|sc</code></td></tr><tr><td>Prover9 の秒</td><td colspan="3">10</td></tr><tr><td>Vampire の秒</td><td>書いていない（査読の既定 20）</td><td>20</td><td>90</td></tr></table>
txt <code>backend p=prover+ v=vampire+ s=satallax+ h=hyperion</code> … 投げ先の文字と backend の対応。
txt <code>target p v s h</code> … この環境で使える投げ先。
txt <code>sort s c</code> … 多ソートの型として宣言するソート。
txt <code>translate 0 sc</code> … 使う翻訳。
txt <code>inference goal -| sos &lt;-&gt; (goal ◀ sos)|cvt+|0</code> … 関係の定義（この行が無い関係は使えません）。
txt <code>prover9 search:seconds 10</code>、<code>vampire search:seconds 20</code> … 1回の問題を待つ秒数。
txt <code>prover+ problem:split</code> / <code>problem:whole</code> … goal を割るかの既定（段ごとの <code>p[whole];</code> が優先）。

0_tutorial_AI/1.book

`0_tutorial_AI/1.book`