Up 6.2.2 文変形システム  

　Gの上の文変形システム U＝( S, D) は，以下のようになる：

  1. Gのシェマシステム S＝( G,σ, R) では，

    1. G＝( NＶ, TＶ, Ｐ, SEN) は，
      NＶ：
        SEN：文シェマ生成に関する
        SVR：文記号生成に関する(註1)

      TＶ＝TＶ∪{sen，1}

      Ｐ：
        SEN → (SEN)∧(SEN)
        SEN → (SEN)∨(SEN)
        SEN → (SEN)⊃(SEN)
        SEN → (SEN)(SEN)
        SEN → ¬(SEN)

        SEN → (SVR)
        SVR → SVR1
        SVR → sen

    2. σ：
        SEN → SEN

    3. R＝φ

  2. D：
    1. 変形補助記号は無し。

    2. 文変形規則は，以下のもの(註2)：

        (C1) ¬(¬(sen)) ﾌ sen
        (C2) sen∧sen1 → sen1∧sen
        (C3) ¬((¬sen)∧(¬sen1)) ﾌ sen∨sen1
        あるいは，同じこととして(註3)，
        sen∧sen1 ﾌ ¬((¬sen)∨(¬sen1))
        (C4) ¬(sen∧¬sen1) ﾌ sen⊃sen1
        あるいは，同じこととして(註4)，
        sen∧sen1 ﾌ ¬(sen⊃¬sen1)
        (¬sen)∨sen1 ﾌ sen⊃sen1
        sen∨sen1 ﾌ ¬sen⊃sen1
        (C5) (sen⊃sen1)∧(sen1⊃sen) ﾌ sensen1


（註１） SVR（Sintence-VaRiable) から，文記号
(sen)，(sen1)，(sen11)，････
が生成されることになる。
　非終端記号 SVR に関するプロダクションは，‘ξ23’のように記号列を一つの変数として使用するわれわれの通常の実践の定式化になっている。
　このように記号列を変数として使えるようにするときは，‘ξ23’の‘ξ2’に対して代入が行なわれるようなことがないように，対処しなければならない。
　これは，TＶに括弧：
（，　）
を含ませ，生成されるシェマ変数が括弧で括られた記号列になるようにすることで，処置できる。プロダクションの
SEN → (SVR)
の括弧には，このような意味がある。（もちろん，シェマ変数として記号列を用いないことにすれば，このような措置は必要ない。）
　以下の記述では，煩瑣を避ける意味から，この措置のための括弧の表示は適宜省略する。

（註２） (C3) から (C5) までは，∨，⊃， を簡約記号として導入することに対応するもの。


（註３） (C1) より，¬(¬sen∧¬sen1) ﾌ sen∨sen1 のとき，sen∧sen1 ﾌ ¬¬(¬¬sen∧¬¬sen1) ﾌ ¬(¬sen∨¬sen1)。
逆に，sen∧sen1 ﾌ ¬(¬sen∨¬sen1) のとき，¬(¬sen∧¬sen1) ﾌ ¬¬(¬¬sen∨¬¬sen1) ﾌ sen∨sen1。

（註４） (C1) による。