演繹シリアル化構文と実行モデル。

環境として、論理環境（logical environment）と応用固有環境（application-specific environment）がある。論理環境は、論理定理データベースと論理推論規則データベースからなる。応用固有環境は、応用固有定理データベースと応用固有推論規則データベースからなる。「論理→応用固有」は環境チェーンだが、環境はツリーに編成できる。環境ツリーの末端がオブジェクトレベルで、ルート方向にたどると、メタ、メタメタ、メタメタメタなどとなる。環境ツリーのルートを原始論理（primitive logic）または原論理（proto-logic）と呼ぶ。

コマンドの実行状態は証明オブジェクトだが、証明オブジェクトはストリング図（ストリンググラフ）で表現される。

コマンドの引数は、参照引数、暗黙引数（省略）、リテラル（即値）引数がある。式パスを引数に使うこともある。コマンドにはその結果命題（result）があり、コマンドの直後に結果を書く。

コマンドの実行時にカレント論理式が1つあり、カレント論理式はthisで参照される。thisは暗黙の引数に使われる。コマンドが実行されると結果が生成されて、その結果を使って証明オブジェクト（ストリング図）が更新され、thisが結果に置き換わる。

推論規則	書き方
公理引用	単純コマンド 1引数
∧導入	単純コマンド 2引数
∧除去	単純コマンド 1引数 パス
∨導入	単純コマンド 2引数
∨除去	ブロック 1引数 結果はブロック内の最後の結果
⇒導入	ペアコマンド 0引数 2引数
⇒除去	単純コマンド 2引数
¬導入	ブロック 1引数 結果はブロック終了の後に書く。
¬除去	単純コマンド 2引数 結果はFalse（⊥）
⊥導入	(¬除去と同じ)
⊥除去	単純コマンド 1引数
∀導入	ブロック＋単純コマンド 1引数
∀除去	単純コマンド 1引数
∃導入	単純コマンド 2引数（1つは証拠項）
∃除去	ブロック 1引数 結果はブロック内の最後の結果

ブロック構文は：

1. ∨除去 casesブロック
2. ¬導入 contradictionブロック
3. ∀導入 forブロック
4. ∃除去 choiceブロック

Mizarだと、∃除去に consider x such that P を使うらしいが、イマイチ分かりにくい。takeと区別しにくいし。