Page 24 - MATINF Nr. 4

24 D. Constantin, A.F. S , tefan

Secvent , ii etichete ale vˆarfurilor arborelui T sunt:

ϕ (r) = S,

ϕ (n 1 ) = {β, ((¬α) → γ)} =⇒ {(β ∨ γ)} ,
ϕ (n 2 ) = {((¬α) → γ)} =⇒ {α, (β ∨ γ)} ,
ϕ (n 3 ) = {β, γ} =⇒ {(β ∨ γ)} ,
ϕ (n 4 ) = {β} =⇒ {(¬α) , (β ∨ γ)} ,
ϕ (n 5 ) = {β, γ} =⇒ {β, γ} ,

ϕ (n 6 ) = {α, β} =⇒ {(β ∨ γ)} ,
ϕ (n 7 ) = {α, β} =⇒ {β, γ} ,
ϕ (n 8 ) = {γ} =⇒ {α, (β ∨ γ)} ,
ϕ (n 9 ) = Ø =⇒ {(¬α) , α, (β ∨ γ)} ,
ϕ (n 10 ) = {γ} =⇒ {α, β, γ} ,
ϕ (n 11 ) = {α} =⇒ {α, (β ∨ γ)} .

Pentru construirea unui arbore de demonstrat , ie asociat unui secvent dat S se poate utiliza
algoritmul de deduct , ie logic˘a bazat pe regulile de inferent , ˘a Gentzen.

2.2 Algoritmul de deduct , ie logic˘a bazat pe regulile de inferent , ˘a Gentzen

Deduct , ie Logic˘a Gentzen DLG(S)
Init , ializ˘ari: Arborele curent T = (V (T) , E (T)), cu V (T) = {r} , ϕ (r) = S, E (T) = Ø.
Repeat
P1: Se selecteaz˘a un vˆarf n aflat pe frontiera arborelui curent astfel ˆıncˆat ϕ (n) nu este secvent
ˆıncheiat s , i ϕ (n) nu este secvent axiom˘a
P2: Se selecteaz˘a o formul˘a α /∈ V din antecedentul/succedentul secventului ϕ (n) s , i se identific˘a
regula Gentzen (notat˘a R G ) aplicabil˘a formulei α
P3: (i) Dac˘a regula R G este de tipul 1, reprezentat˘a prin S 1 atunci se reactualizeaz˘a arborele
ϕ(n)
T prin
T ← (V (T) ∪ {n 1 } , E (T) ∪ {nn 1 })

unde
n 1 /∈ V (T) , ϕ (n 1 ) = S 1
(ii) Dac˘a regula R G este de tipul 2, reprezentat˘a prin S 1 ,S 2 atunci se reactualizeaz˘a
ϕ(n)
arborele T prin
T ← (V (T) ∪ {n 1 , n 2 } , E (T) ∪ {nn 1 , nn 2 })
unde

n 1 , n 2 /∈ V (T) , ϕ (n 1 ) = S 1 , ϕ (n 2 ) = S 2
Until (exist˘a cel put ,in un secvent ˆıncheiat care nu este axiom˘a) sau (toate vˆarfurile aflate pe
frontiera arborelui curent generat au ca etichete secvent ,i axiom˘a)
If (exist˘a cel put ,in un secvent ˆıncheiat care nu este axiom˘a) Then write(Secventul S nu este
demonstrabil)
If (toate vˆarfurile aflate pe frontiera arborelui curent generat au ca etichete secvent ,i axiom˘a)
Then write(Secventul S este demonstrabil)