Up 6.2.3 推論システム  

　U＝( S, D) は，つぎのようになる。
  1. Sは， S#＝( G#,σ#, R) の G#に対し，終端記号に

    txt

    を追加し，プロダクションに

    TXT → TXT1
    TXT → txt
    を追加したもの。

  2. Dでは，

    1. テクスト変形補助記号は無し。

    2. テクスト変形規則は，“命題論理の公理”：

        (S1) ε → sen ⊃ (sen1⊃sen)
        (S2) ε → (sen⊃(sen1⊃sen11)) ⊃ ((sen⊃sen1)⊃(sen⊃sen11))
        (S3) ε → (¬sen1⊃¬sen)⊃ (sen⊃sen1)

      と，“分離規則(Modus Ponens)”：

        (MP)“sen と sen⊃sen1 から sen1 が導かれる"(註)

      と，そしてDが定める文変形規則から導かれるもの。



（註） “senとsen→sen1からsen1が導かれる"は，簡約化した言い方であり，これをきちんと述べるならば，以下のようになる：

(1)　＾sen＾txt＾sen⊃sen1＾txt1/ 　→　＾sen＾txt＾sen⊃sen1＾txt1＾sen1/
(2)　＾sen＾txt＾sen⊃sen1/ 　→　＾sen＾txt＾sen⊃sen1＾sen1/
(3)　＾sen＾sen⊃sen1＾txt/ 　→　＾sen＾sen⊃sen1＾txt＾sen1/
(4)　＾sen＾sen⊃sen1/ 　→　＾sen＾sen⊃sen1＾sen1/
(5)　 /sen＾txt＾sen⊃sen1＾txt1/ 　→　/sen＾txt＾sen⊃sen1＾txt1＾sen1/
(6)　 /sen＾txt＾sen⊃sen1/ 　→　/sen＾txt＾sen⊃sen1＾sen1/
(7)　 /sen＾sen⊃sen1＾txt1/ 　→　/sen＾sen⊃sen1＾txt1＾sen1/
(8)　 /sen＾sen⊃sen1/ 　→　/sen＾sen⊃sen1＾sen1/

ここで，/ は，テクストの端を表わすメタ記号。