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

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

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

基本証明のストック：

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

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