Page 25 - MATINF Nr. 4

Elemente computat , ionale de deduct , ie logic˘a 25

Observat ,ia 8. Pentru efectuarea pasului P1 este necesar˘a verificarea etichetelor vˆarfurilor aflate
pe frontiera arborelui curent generat (adic˘a etichetele vˆarfurile terminale sau frunzele din arborele
T). Dac˘a exist˘a cel put , in un secvent ˆıncheiat care nu este axiom˘a atunci se decide terminarea
procesului de reactualizare a arborelui T cu decizia Secventul S nu este demonstrabil. Dac˘a
toate vˆarfurile aflate pe frontiera arborelui curent generat au ca etichete secvent , i axiom˘a, atunci
arborele curent generat este un arbore de demonstrat , ie pentru secventul init , ial S s , i ˆın acest caz
procesul de reactualizare se ˆıncheie cu decizia Secventul S este secvent demonstrabil s , i astfel se
deduce demonstrabilitatea mult , imii de formule din succedent (Γ) pe baza mult , imii de formule
din antecedent (H).
Exemplul 7. Algoritmul de deduct , ie logic˘a Gentzen se aplic˘a pentru secventul de la exemplul 6.
Se noteaz˘a cu ∂T frontiera arborelui T.
Init , ial avem T = ({r} , Ø) , iar ϕ (r) = {(α → β) , ((¬α) → γ)} =⇒ {(β ∨ γ)}.
Etapele de reactualizare a arborelui T prin aplicarea algoritmului de deduct , ie logic˘a bazat
pe regulile de inferent , ˘a Gentzen sunt:
1. ∂T = {r} , n = r; formula selectat˘a (α → β) ; se aplic˘a regula G4;

n 1 n 2
T : -%
r
ϕ (n 1 ) = {β, ((¬α) → γ)} =⇒ {(β ∨ γ)} , ϕ (n 2 ) = {((¬α) → γ)} =⇒ {α, (β ∨ γ)}.
2. ∂T= {n 1 , n 2 } ; n = n 1 ; formula selectat˘a ((¬α) → γ) ; se aplic˘a regula G4;

n 3 n 4
-%
T : n 1 n 2
-%
r

ϕ (n 3 ) = {β, γ} =⇒ {(β ∨ γ)} , ϕ (n 4 ) = {β} =⇒ {(¬α) , (β ∨ γ)}.
3. ∂T= {n 3 , n 4 , n 2 } ; n = n 3 ; formula selectat˘a (β ∨ γ) ; se aplic˘a regula G7;

n 5
↑
n 3 n 4
T : -%

n 1 n 2
-%
r

ϕ (n 5 ) = {β, γ} =⇒ {β, γ} este secvent axiom˘a.
4. ∂T= {n 5 , n 4 , n 2 } ; n = n 4 ; formula selectat˘a (¬α) ; se aplic˘a regula G5;

n 5 n 6
↑ ↑
n 3 n 4
T : -%

n 1 n 2
-%
r
ϕ (n 6 ) = {α, β} =⇒ {(β ∨ γ)}.