リーズニング・コンビネータ

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある：

1. 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。
2. 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。
3. 選言除去用コンビネータ： 既存のn個の証明から連言からの証明を作る。
4. 存在除去用コンビネータ： 既存のパラメータ付き証明から存在からの証明を作る。
5. 含意導入用コンビネータ： 既存の前提あり証明から含意命題への証明を作る。カリー化／ラムダ抽象。
6. 否定導入用コンビネータ： 既存の偽への証明から否定命題を作る。ド・モルガン作用素。
7. 帰納法用コンビネータ： 既存の帰納法のベース・ステップ証明から帰納的証明を作る。

基本証明のストック：

1. 連言除去証明： 射影、フィールド参照。ポスト結合する。
2. 選言導入証明： 入射、値コンストラクタ。単体提示またはプレ結合する。
3. 存在導入証明： 事例、パラメータ＝束縛変数の特定値、個体で閉じた命題。単体提示またはプレ結合する。
4. 含意除去証明： 評価射、モーダスポネンス。ポスト結合する。
5. 否定除去証明： モーダスポネンスで矛盾（真ならば偽）生成、メタ背理法。異質。

バックワードが困難なコンビネータにはアスタリスク：

作成目標	基本証明	コンビネータ	ステージ
連言への証明		◯ペアリング	◯
連言からの証明	◯射影	◯後結合*
選言への証明	◯入射	◯前結合、挿入
選言からの証明		◯直和	◯
全称への証明		◯依存カリー化	◯
全称からの証明	◯一般射影	◯後結合*
存在への証明	◯一般入射	◯前結合、挿入
存在からの証明		◯依存余カリー化	◯
含意への証明		◯カリー化	◯
含意からの証明	◯評価	◯後結合*
真への証明	◯自明	◯後結合*
真からの証明
偽への証明		◯否定生成	◯
偽からの証明	◯自明	◯前結合、挿入