book集

section MatheliaとBook
txt Matheliaは堅牢な数学を作成するためのソフトです。
txt 数学を書くための記法、本として読ませる表現、証明を確かめる仕組み、が一つにまとまっています。
txt 数学作成時の使い方の基本は 数学を書く → 表示を確認する → 機械に査読してもらう の繰り返しとなるでしょう。
br
txt 数学はBookというものに書かれます。 .bookファイル に記録され、表示ソフトで閲覧されます。
txt Bookには通常、数学記号の紹介や定義、定理とその証明、などデータが書かれていきます。
br
txt Bookは .bookファイルの仕様 に従って書かれねばなりません。
txt それはヘッダと本文からなり、両者は --- という行で区切られます。ヘッダと本文の各行は原則として<note>命令語で始まります<?>この行（ソースファイル第14行）は txt という命令語で始まっています。次のページに命令語一覧があります</note>。
txt Book機能の例として、section番号を自動でつけてもらったり、他のBookをimportしデータを引き継いだり、ができます。
txt Bookのコンパイル時には「書法にエラーが無く表示ができるか？」「他ファイルの読み込みはちゃんとできるか？」などがチェックされます。
br
txt ★Matheliaの仕様はまだ未確定のものも多いです。使用された方からの「こういう機能が欲しい」という建設的な意見をお待ちしております。
txt ★Matheliaは人間よりむしろAIに使用してもらうことが想定されています。人間はできたBookを鑑賞するものです！？

section Bookの査読
txt Bookを表示させると、各頁に査読（この頁）ボタンが出てきます(このBookには査読すべき対象が無いため出てきません)。押すと、紹介査読（記号や Prop が使う前に紹介されているか）と Thm査読（証明が正しいか）が続けて行われ、両方 OK なら「査読: ALL OK」と出ます。
txt 査読はMatheliaの最も重要な機能で、「まだ紹介されてない記号が無いか？」「証明が正しいか」などを、文字通り「機械的に」チェックします。
txt それは、上から順に、そのBook（とimportされたBook）の「その位置までに紹介されたもの」に書かれていることだけで行われます。
txt なおtxt行は人間のための説明であり査読では無視されます。
txt 例えば、紹介していない word を Thm の中で使うと、その Thm は査読で FAIL（未紹介の word）になります。backend が証明できなかった Thm も FAIL です。
txt また査読されるのは保存済みの .book です。結果は頁ごとに保存され、前の頁やimportした本の査読はやり直さずに結果を拾います。

section Matheliaの部品
txt Matheliaは内部で独立性の高い部品を多く持っています。
txt 〇DB (データベース)は様々なデータを保存します。
txt 〇数学の記述においては、Form（項や命題を表す記号の列）を扱う Formel、Thm（「goal が sos から推論できる」という形の主張）を扱う Thmel が使用されます（詳しくは2.book, 3.book）。
txt 〇Thmを査読する backend(prover+, vampire+, satallax+, hyperion) はMatheliaの心臓部と言えます。
txt さらに 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の堅牢さを保証するためには、各部品を堅牢にし、部品間の情報のやり取りの流れを明瞭にすることが大事です。

newpage

section 命令語とオプションの一覧
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 の宣言です（AI 用 tutorial の 0_tutorial_AI/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>goal -| +結合則 p;</code>
txt 投げ先の文字は .thmel の backend が決めます（p＝prover+、v＝vampire+、s＝satallax+、h＝hyperion）。投げ先は <code>;</code> の直前に空白なしで付けます。投げ先の無い段は査読エラーです。
txt <code>p[whole];</code> … goal を断片に割らずに1つの問題として投げます。
txt 投げた段が〇になると、その段の 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）。
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 の 3・4.book）、common/default.thmel（標準）、common/zf.thmel（default と同じで Vampire の待ち時間だけ長い）です。
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> が優先）。

section CLIから査読する
txt ブラウザの査読ボタンを押せない場合（AIエージェントが対話画面を持たずに作業しているときなど）は、Web画面と全く同じ査読をCLIから実行できます。
txt <code>cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/review_cli.php &lt;本の名前&gt; [頁番号]</code>
txt &lt;本の名前&gt;はフォルダ名/本の名前（拡張子なし。例 standard_math/1）。頁番号は省略可能な引数です（「option review per-page:false;」を宣言した本では効きません）。
txt 査読ボタンと同じく紹介査読と Thm査読を続けて行い、紹介査読の件数（落ちた行があれば行番号と理由）、各Thmの番号・結果（OK／FAIL、FAILなら理由）、全体の判定（ALL OK／FAIL）をプレーンテキストで返します。終了コードは0＝ALL OK、1＝FAILあり、2＝引数や本の指定の誤り、3＝判定できない（コンパイルエラーなど）です。
txt 自分で書いたThmが正しいかをその場で確かめたいときは、まずこのコマンドを使ってください。

0_tutorial/1.book

`0_tutorial/1.book`