book集

section Thmelの基本
subsection prop, Thm
txt p-Formの間の推論関係を扱うソフトが Thmel です。
txt ヘッダで .thmel ファイルを指定すると使用できます。このBookでは thmel min とあり min.thmel が読み込まれます。
txt Thmの eval は各propを Formel に投げ<code>FCL</code>に変換したものです。
br
txt Thmel の定数として Formel のp-Formを登録したものをpropと言います。
txt prop ${\tt P}$ とpropの列 $\Gamma$ に対し ${\tt P}$ ◀ $\Gamma$ の形のものをThmと言います。${\tt P}$をgoal、$\Gamma$をsosと言うことがあります。
txt 例えば　`⊤` ◀ O　はThmです。O は空の列です。
br
txt Propは DB に登録されてあるものを使う他に、自分で prop名 &lt;- `…` と書いて作ることもできます。
txt Prop ${\tt P}$ が指すp-FormをForm内で使用したいときは @${\tt P}$ とします。<note>使えるのはThmの中だけです<?>Thmの eval の最初に行います。なお、その位置までに紹介したpropだけを取り出せます。</note>。乱用しない方が良いです。

subsection Thmの変換
txt ThmをThmに変換することがMatheliaでは重要です。backendごとに扱える論理が違う（次の節）ので、Thmをそのbackendが扱える言語のThmに変換してから投げるためです。
txt 最も簡単な例として、所属言語の変換を挙げます。
txt Formは高階{s,c}ソート言語です。それとは別に「高階言語」があるとみなし、Thmの変換 <code>|0</code> を作ります。
txt 　$\mathcal{T}$が部分Formとしてc-Formを含んでいなければ $\mathcal{T}$<code>|0</code> = ($\mathcal{T}$を高階言語に自然に翻訳したもの)、そうでなければ $\mathcal{T}$<code>|0</code> はエラー
txt 高階言語のThmは ◀ ではなく ◁ を使って作ります（説明でしか使わない記号）。また、違う言語であることを明示したいときなどにFormを緑にします。
txt 例　(`⊤` ◀ O)<code>|0</code> $=$ ‘⊤‘ ◁ O
txt 一般にThm $\mathcal{T}$とThm変換<code>|f</code>に対して、$\mathcal{T}$<code>|f</code> の eval は、$\mathcal{T}$を eval してから<code>|f</code>を計算したものです。

section 定理
subsection 論理
txt Thmは形式的なものです。Thmに意味を与えるものを論理と言います。
txt Thm $\mathcal{T}$ を論理 $\mathbb{L}$ で扱うことができ ◀ を「推論できる」と読めるとき $\mathcal{T}$ holds in $\mathbb{L}$ と書きます。
txt Matheliaでは 高階{s,c}ソート論理 $\mathbb{L}_{\rm Hsc}$ と 高階論理 $\mathbb{L}_{\rm H}$ は既知のものとされます。
txt 通常はそれらの部分論理である、一階{s,c}ソート論理 $\mathbb{L}_{\rm 1sc}$ と 一階論理 $\mathbb{L}_1$ が使用されます。
txt なお例えば $\mathbb{L}_1$ の公理には 等号公理、領域の非空性公理 ‘∃ x \, (x = x)‘ が含まれます。
br
txt backend が「$\mathbb{L}$ を判定する」とは「Thm $\mathcal{T}$ を受け取ったとき、$\mathcal{T}$ holds in $\mathbb{L}$ を確かめると 〇 を返す」事です。
txt ★各backendが判定する論理
txt 　prover+ … $\mathbb{L}_1$（一階論理）
txt 　vampire+ … $\mathbb{L}_\mathrm{1sc}$（一階{s,c}ソート論理）
txt 　satallax+ … $\mathbb{L}_\mathrm{Hsc}$（高階{s,c}ソート論理）

subsection 定理とそのprf
txt 一般に Thmel は $\mathbb{L}_*$ という論理を規定します。$\mathcal{T}$ holds in $\mathbb{L}_*$ という形のものを「定理」と呼ぶべきです。
txt min.thmelは次のように規定しています。
txt 　$\mathcal{T}$ holds in $\mathbb{L}_*$ $\Longleftrightarrow$ $\mathcal{T}$ holds in $\mathbb{L}_\mathrm{Hsc}$
txt 　$\mathcal{T}$<code>|0</code> がエラーでなければ　$\mathcal{T}$ holds in $\mathbb{L}_*$ $\Longleftrightarrow$ $\mathcal{T}$<code>|0</code> holds in $\mathbb{L}_\mathrm{H}$
br
txt BookではThmの後にはprfが書かれます（表示はされないのでprfの議論になったときは直接ソースファイルを見て下さい）。
txt $\mathcal{T}$というThmの後のprfは $\mathcal{T}$ holds in $\mathbb{L}_*$ の証明とみなせるものです。
txt prfはThm査読において査読器に見てもらうものです。 backendの略記法が使用されます：p=prover+ v=vampire+ s=satallax+ h=hyperion
txt prfには例えば ${\tt P}$ ◀ $\Gamma$ v; という記述がされます。「${\tt P}$ ◀ $\Gamma$ を v に投げる」と読みます。査読器はそれを見ると ${\tt P}$ ◀ $\Gamma$ を eval し vampire+ に投げます。
br
txt min.thmelには次の略記法も指定されています。
txt 　${\tt P}$ -| $\Gamma$ … (${\tt P}$ ◀ $\Gamma$)<code>|0</code>
txt 正確には、.thmel には (P ◀ Γ)<code>|cvt+|0</code> と書かれています。<code>|cvt+</code> は 5.book で導入する変換で、c-Form を含まない Thm は変えません。この Book の範囲では (P ◀ Γ)<code>|0</code> と同じです。
txt prfには ${\tt P}$ -| $\Gamma$ p; という記述もよくされます。査読器はそれを見ると ${\tt P}$ -| $\Gamma$ を eval し prover+ に投げます。

newpage

section 定理の例
subsection prover+に投げる
txt prover+ は(一階言語の)Thmを受け取るとProver語に変換してProver9に投げます。最初のThmを作ってみます。
thm `⊤` ◀ O
prf `⊤` -| O p;
txt この査読においては prover+ は<note>コレ<?>formulas(sos).end_of_list.formulas(goals).$T.end_of_list.</note>を作ってProver9に投げます(`⊤` は $T になっています)。
txt 実際に下の右側の「査読」ボタンを押してみて！
txt 「OK」と出てくるはず。#列の 3-1 は section3の1番目のThm という意味です。
txt そしてOKをクリックすると「Prover9が length:2 の証明を見つけた」事が分かります。
br
word +
prop +結合則 <- `x + (y + z) = (x + y) + z`
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf goal -| +結合則 p;
txt 今度は<note>コレ<?>formulas(sos).(plus(x,plus(y,z)) = plus(plus(x,y),z)).end_of_list.formulas(goals).(plus(x,plus(y,plus(z,w))) = plus(plus(plus(x,y),z),w)).end_of_list.</note>がProver9に投げられ、length:5 の証明が見つかります。
txt Prover9への入力には `+` のgramが(ss,s)であることは書きません。

subsection vampire+に投げる
txt vampire+ は(一階{s,c}ソート語の)Thmを受け取るとTFF形式に変換し記号のハッシュ化をしてVampireに投げます。上のThmに違うprfを付けてみます。
thm `⊤` ◀ O
prf `⊤` ◀ O v;
txt この査読においては vampire+ は<note>TFF形式<?>tff(mathel_s_type, type, mathel_s: $tType). tff(mathel_c_type, type, mathel_c: $tType). tff(mathel_conjecture, conjecture, $true).</note>(`⊤` は $true に)を作りそのままVampireに投げます。
txt min.thmelには sort s c とあり <code>mathel_s</code> <code>mathel_c</code> が型として宣言されています。
br
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf goal ◀ +結合則 v;
txt 今度は<note>TFF形式<?>tff(mathel_s_type, type, mathel_s: $tType). tff(mathel_c_type, type, mathel_c: $tType). tff(plus_type, type, plus: (mathel_s * mathel_s) > mathel_s). tff(mathel_axiom_1, axiom, ! [X: mathel_s, Y: mathel_s, Z: mathel_s] : ((plus(X, plus(Y, Z)) = plus(plus(X, Y), Z)))). tff(mathel_conjecture, conjecture, ! [W: mathel_s, X: mathel_s, Y: mathel_s, Z: mathel_s] : ((plus(X, plus(Y, plus(Z, W))) = plus(plus(plus(X, Y), Z), W)))).</note>では <code>plus: (mathel_s * mathel_s) > mathel_s</code> という型宣言がされています。

subsection satallax+に投げる
txt satallax+ は(高階{s,c}ソート語の)Thmを受け取るとTHF形式に変換してSatallaxに投げます。
thm `⊤` ◀ O
prf `⊤` -| O s;
txt 受け取った satallax+ はTHF形式<note>コレ<?>thf(goal, conjecture, $true).</note>を作りSatallaxに投げます。
br
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf goal -| +結合則 s;
txt 今度は<note>コレ<?>thf(ty_plus, type, plus: $i > $i > $i). thf(axiom_1, axiom, ( ! [X:$i,Y:$i,Z:$i] : (((plus @ X @ (plus @ Y @ Z)) = (plus @ (plus @ X @ Y) @ Z))) )). thf(goal, conjecture, ( ! [X:$i,Y:$i,Z:$i,W:$i] : (((plus @ X @ (plus @ Y @ (plus @ Z @ W))) = (plus @ (plus @ (plus @ X @ Y) @ Z) @ W))) )).</note>がSatallaxに投げられます。関数記号もλ計算のカリー化（<code>plus @ X @ Y</code>）で書かれ、Prover9・Vampireの一階項 <code>plus(X,Y)</code> とは形が違います。

subsection 違い
txt 以上のThmの査読においては、
txt 　Prover9の計算時間は7ms程ですが、これはほぼプロセス起動の分だけで、探索時間はほぼ0のハズ
txt 　Vampireの計算時間は10ms程ですが、これもほぼプロセス起動の分だけで、探索時間はほぼ0のハズ
txt 　Satallaxの計算時間は、`⊤` ◀ O では10ms程ですが、もう一つでは600ms程かかります。
txt Satallaxは常にHOLの証明探索をするため、この一階の内容には割に合わないコストがかかります。
txt 一階の（簡単な問題では差が出ませんが）難しい問題ではProver9とVampireで得意・不得意が出てきます。
txt どういうときにどの backend に投げるかは、実測の例とともに AI 用 tutorial の 0_tutorial_AI/6b.book（実践：投げ先・失敗・戦略）にまとめています。
txt -| はいつも意味を持つとは限りません。<code>|0</code> はエラーを返すことがあるので。

section 2ソート定理の例
txt s-Formを「もの(の種類)」、c-Formを「箱」と見なし、「入っている」を表すwordを準備します。
word ∈_
txt 1つの箱 `X_` は、ものを「`X_`に入っている／いない」の2通りに分けます。1つの箱だけでは3点の区別はできません（鳩の巣原理）。
thm `¬ \\{ And x1 ∈_ X_ {/}⇔ x2 ∈_ X_ \\ x2 ∈_ X_ {/}⇔ x3 ∈_ X_ \\ x3 ∈_ X_ {/}⇔ x1 ∈_ X_ \\}` ◀ O
prf goal ◀ O v;
br
txt Hallの定理（各箱から異なるものを選べる条件）の小さな具体例です。3つの箱に何が入っているかを具体的に与え、そこから「各箱から異なるものを1つずつ選べる」ことを示します。
prop Hall <- `\\{ And [ |p ; |q col ∈_ |A_ ] \\ [ |q ; |r col ∈_ |B_ ] \\ [ |r ; |p col ∈_ |C_ ] \\}`
prop neq <- `|p {/}= |q and |q {/}= |r and |r {/}= |p`
thm `[ ∃ x ∈_ |A_ . [ ∃ y ∈_ |B_ . [ ∃ z ∈_ |C_ . ( x {/}= y and y {/}= z and z {/}= x ) ] ] ]` ◀ Hall ,, neq
prf goal ◀ Hall ,, neq v;
txt Vampireは一瞬で割り当て（`|A_`→`|p`, `|B_`→`|q`, `|C_`→`|r` など）を見つけます。

newpage
section {s,c}ソート言語のThmをprover+に投げる（参考）

subsection 教科書の復習：多ソートとソート無しの論理について
txt まず、各ソート <code>a</code> について、元の言語に無い一項述語 <code>:a</code> を新しく作ります。
txt ${}^{*}$ を相対化とします … <code>x</code> のソートが <code>a</code> のとき <code>∀ x P</code> は <code>∀ x (x:a ⟹ P)</code> に、<code>∃ x P</code> は <code>∃ x (x:a and P)</code> にします。
txt 定理　多ソート言語の文 ${\tt P}$ と、文の集まり $\Gamma$ について
txt 　$\Gamma$ から ${\tt P}$ が推論できる（多ソート）　$\Longleftrightarrow$　Ax と $\Gamma^{*}$ から ${\tt P}^{*}$ が推論できる（ソート無し）
txt Ax は 各ソートは空でないこと（<code>∃ x (x:a)</code>）と、記号の型付け（<code>f</code> のgramが <code>(a,b)</code> なら <code>x:a ⟹ fx:b</code>） です。

subsection 一階翻訳
txt 一階{s,c}ソート言語のThmの一階翻訳 とは「全称量化し、相対化して、Axを添えた一階言語のThm」です。
txt 全称量化 … `x` が自由に出現していれば `∀ x` を先頭につけ、 `X_` が自由に出現していれば `∀_ X_` を先頭につける。
txt Axについては実際に出てくるソートと記号についてだけ添えられます。なお<note>ソートが互いに素であること<?>「集合であってクラスでもあるものは無い」というような主張です。</note>を添えることはありません。
txt `⊤` ◀ O の一階翻訳は ‘⊤‘ ◁ O です。
br
txt ★prover+ は$\mathbb{L}_\mathrm{1sc}$も判定します。一階{s,c}ソート言語のThmを受け取ったときは、まず一階翻訳をします。
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf goal ◀ +結合則 p;
txt このprfの査読では、prover+はまず一階翻訳をして
txt 　‘∀ x ∀ y ∀ z ∀ w \, (x :s and y :s and z :s and w :s ⟹ x + (y + (z + w)) = ((x + y) + z) + w)‘
txt 　◁ ‘∃ x \, (x :s)‘，‘∀ x ∀ y \, (x :s and y :s ⟹ x + y :s)‘，‘∀ x ∀ y ∀ z \, (x :s and y :s and z :s ⟹ x + (y + z) = (x + y) + z)‘
txt とします。さらに<note>コレ<?>formulas(sos).exists xnes (msort_s(xnes)).all a1 all a2 ((msort_s(a1) & msort_s(a2)) -> (msort_s(plus(a1, a2)))).all x all y all z ((msort_s(x) & msort_s(y) & msort_s(z)) -> ((plus(x, plus(y, z)) = plus(plus(x, y), z)))).end_of_list.formulas(goals).all w all x all y all z ((msort_s(w) & msort_s(x) & msort_s(y) & msort_s(z)) -> ((plus(x, plus(y, plus(z, w))) = plus(plus(plus(x, y), z), w)))).end_of_list.</note>をProver9に投げ、約400msでlength:18の証明が見つかります。

subsection hyperionにも投げる
txt 次のThmになっても -| … p; や ◀ … v; であれば探索時間1ms未満です。
txt しかし ◀ … p; では100秒待っても探索が終わりません（査読の制限時間は10秒なので、査読では timeout になります）。以下のprfでは補題を作って完遂しています。
thm `x + (y + (z + (w + u))) = (((x + y) + z) + w) + u` ◀ +結合則
prf Le1 <- `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 p;
 Le2 <- `x + (y + (z + (w + u))) = ((x + y) + z) + (w + u)` ◀ Le1 p;
 Le3 <- `((x + y) + z) + (w + u) = (((x + y) + z) + w) + u` ◀ +結合則 p;
 goal ◀ Le2 ,, Le3 p;
 goal ◀ +結合則 h;
txt Prover9の探索時間は約 400ms / 40ms / 15ms / 800ms、証明は length:18 / 14 / 17 / 14 です。
txt Le1を作らずに Le2 ◀ +結合則 p; だと 2200ms・length:20 になってしまいます。補題は重要です。
br
txt prf最終段の末尾の h; は「hyperionに投げる」ことを意味します。
txt hyperionはメタ推論を担当するソフトで、式の証明探索はせず、既に証明されたThmを組み合わせて新しいThmを作ります。
txt ここでは補題の結果をまとめて length:5 の〇を出しています。

section 高階変数の定数化
txt v^-Form, ?v-Form などが高階変数です。それらを含むThm $\mathcal{T}$ に対し、`P^` を `|P^` に置き替えるなどして、定数化したThmを $\mathcal{T}$<code>|v-elim</code> とします。
txt ただし置き換えるwordはもとのThmに存在しないものから選びます。また、異なる高階変数は異なるwordに置き換えます（単射）。
txt Thm単位での変換であり、同じ高階変数はgoal・sosを通じて同じwordに置き換えます。
txt $\mathcal{T}$<code>|v-elim</code> が一階言語のThmになるなら、置き換え先の選び方によらず 　$\mathcal{T}$ holds in $\mathbb{L}_{\rm H}$ $\Longleftrightarrow$ $\mathcal{T}$<code>|v-elim</code> holds in $\mathbb{L}_1$
txt これは一階論理の「解釈を決めていない記号について示せたことは、その記号を何にしても成り立つ」という事実によります。
br
txt prover+・vampire+は高階変数を含むときは、まず <code>|v-elim</code> をすることで、$\mathbb{L}_{\rm H}$・$\mathbb{L}_{\rm Hsc}$ も一部判定します。
thm `⊥ ⇒ P^` ◀ O
prf `⊥ ⇒ P^` ◀ O v;
txt <code>|v-elim</code> をすると `⊥ ⇒ |P^` ◀ O。

0_tutorial/3.book

`0_tutorial/3.book`