アクツェル推論系と不動点とアリーナ計算

確かムーアは論理式の集合の上の閉包作用素として演繹系を定義したと思う。アクツェルの推論系〈inference system〉の定義は以下のよう：

• 判断〈judgement〉の集合 U
• 演繹ルール〈deduction rule〉は A⊆U と c∈U の組 (A, c) 、これを A/c とも書く。
• A を演繹ルールの前提達〈premises〉または前件達〈antecedents〉の集合と呼ぶ。
• c を結論〈conclusion〉と呼ぶ。
• 演繹ルールの集合を Φ と書く。
• (U, Φ) を推論系とアクツェルは呼ぶ。

当然に同義語がたくさんあって：

• 判断＝命題＝論理式＝文
• 演繹ルール＝推論ルール〈規則〉＝推論可能性の生成元
• 前提／前件＝仮定＝仮説
• 結論＝帰結
• 推論系＝演繹系＝証明系＝論理系

アクツェル推論系のワンステップ演繹演算子 φ を次のように定義する

• For S∈Pow(U), φ(S) := {u∈U | ∃A⊆S. (A, c)∈Φ }
• Φ: Pow(U) → Pow(U)

Pow(U) は完備順序集合なので、Φに対する不動点の議論ができる。

それはそうと； Φをインデックス集合とみて、演繹ルールを判断〈命題〉で型付けされたカローラとみなす。すると、演繹ルールはU-色付きカローラとなる。色を保存するフィッティング関数による接ぎ木が推論の結合〈合成〉になる。したがって、証明木をツリーとするアリーナ計算ができる。

アリーナ	論理	代数指標
カローラ	基本推論規則	オペレーション
アリーナ	推論規則キット	指標
ツリー	証明	項
フォレスト	知識DB	割り当て〈代入〉系
リーフ	仮定の命題ラベル	変数
ルート	結論の命題ラベル	項の名前
中間ノード	中間の推論	括弧囲み部分項
高さ0ツリー	公理	定数
接ぎ木	リーズニングn	置換〈代入〉
フラット化	定理化	代入計算
リーフカラー	仮定の命題	変数の型
ルートカラー	結論の命題	項の型

アリーナ計算、コンステレーション〈テンプレート〉計算、論理、代数 が同じ枠組みで記述できる。