形式的に定義しない言葉
- 証明 → 証拠{図 | 式}またはリーズニング{図 | 式}
- 公理 → 原子定理
- 命題 → 論理式、定理
- 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式}
形式的に定義する言葉
- 項、原子項
- 論理式、原子論理式
- 文脈
- シーケント
- 証拠{図 | 式}、原子証拠{図 | 式}
- リーズニング{図 | 式}、原子リーズニング{図 | 式}
- 論理式定理
- シーケント定理
- 論理式定理ライブラリ
- シーケント定理ライブラリ
- 論理式定理ライブラリ・インターフェイス
- シーケント定理ライブラリ・インターフェイス
- 定理のヘッド（名前はオプショナル）
- 定理のステートメント
- 定理のボディ
- 定理／ライブラリのトランスパイル
- 証拠{図 | 式}モナド 単位：論理式の集合 → 証拠図の集合
- リーズニング{図 | 式}モナド 単位：シーケントの集合 → リーズニング図の集合
- モナド変換子： 証拠図モナド → リーズニング図モナド （ゲンツェン変換子）
パターン
