128 3 Der Redehandlungskalkul
Definition 3-2. Subjunktoreinfuhrungsfunktion (SEF)
SEF = {(⅛, X) | Й ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM und i ∈ Dom(⅛), so dass
(ι) A(⅛) = Δ und (i, ⅛) ∈ VANS(M
(ii) A‰m(^1) = Γ,
(iii) Es kein l mit i < l ≤ Dom(⅛)-1 gibt, so dass (l, ⅛l) ∈ VANS(⅛), und
(iv) ⅛, = ʃɔ ∪ {(Dom(⅛), rAlso Δ → Γ∣)}}}.
Vgl. Handlungsanleitung 3-2.
Definition 3-3. Subjunktorbeseitigungsfunktion (SBF)
SBF = {(⅛ X) | ʃɔ ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM, so dass {Δ, r∆ → Γ∣} ⊆
VER(Ej) und ⅛, = Ej ∪ {(Dom(⅛), rAlso Γ∣)}}}.
Vgl. Handlungsanleitung 3-3.
Definition 3-4. Konjunktoreinfuhrungsfunktion (KEF)
KEF = {(⅛ X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ VER(Ej), so dass
⅛' = ⅛ ∪ {(Dom(⅛), rAlso Δ ∧ Γ∣)}}}.
Vgl. Handlungsanleitung 3-4.
Definition 3-5. Konjunktorbeseitigungsfunktion (KBF)
KBF = {(Д X) | Й ∈ SEQ und X = {# | Es gibt Δ, Γ ∈ GFORM, so dass
{r∆ ∧ Γ∣, T ∧ Δ∣} ∩ VER(Ej) ≠ 0 und ⅛' = ⅛ ∪ {(Dom(⅛), rAlso Γ∣)}}}.
Vgl. Handlungsanleitung 3-5.
Definition 3-6. Bisubjunktoreinfuhrungsfunktion (BEF)
BEF = {(⅛ X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ, Γ ∈ GFORM, so dass {r∆ → Γ∣,
T → Δ∣} ⊆ VER(Ej) und ⅛' = ⅛ ∪ {(Dom(⅛), rAlso Δ θΓ∣)}}}.
Vgl. Handlungsanleitung 3-6.
Definition 3-7. Bisubjunktorbeseitigungsfunktion (BBF)
BBF = {(⅛, X) | Ej ∈ SEQ und X = {⅛' | Es gibt Δ ∈ VER(Ej) und Γ ∈ GFORM, so dass
{r∆ θ Γ∣, T θ Δ∣} ∩ VER(⅛) ≠ 0 und ^' = Й ∪ {(Dom(⅛), rAlso Γ∣)}}}.
Vgl. Handlungsanleitung 3-7.